diff options
| -rw-r--r-- | doc/refman/RefMan-mod.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index f4a90740c..505c1110c 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -190,7 +190,8 @@ Defines a module type {\ident} equal to {\modtype}. \end{Variants} -\subsection{\tt Declare Module {\ident} : {\modtype}} +\subsection{\tt Declare Module {\ident} : {\modtype} +\comindex{Declare Module}} Declares a module {\ident} of type {\modtype}. |