From f9b715c4ea07d6ecfece7f28e4d25f3dcab01158 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 24 Nov 2017 23:58:36 +0100
Subject: Document Short Module Printing.

---
 doc/refman/RefMan-mod.tex | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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}}
 
-- 
cgit v1.2.3