Merge PR #6219: Document undocumented options

1 files changed, 5 insertions, 1 deletions

diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index e56c8fa7fe..b4e270e6c3 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}}