diff options
| -rw-r--r-- | doc/refman/RefMan-mod.tex | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index e56c8fa7f..b4e270e6c 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -403,10 +403,14 @@ Fail Check B.T. \end{Warnings} \subsection{\tt Print Module {\ident} -\comindex{Print Module}} +\comindex{Print Module} \optindex{Short Module Printing}} Prints the module type and (optionally) the body of the module {\ident}. +For this command and {\tt Print Module Type}, the option {\tt Short + Module Printing} (off by default) disables the printing of the types of fields, +leaving only their names. + \subsection{\tt Print Module Type {\ident} \comindex{Print Module Type}} |