From 26ddb1e22de1eead0bfb086adf4f2b21dca6ff19 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 14 Jun 2016 15:21:11 -0400
Subject: Add [Unset Printing Dependent Evars Line]

This allows a work-around for bug #4819,
https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
---
 doc/refman/RefMan-oth.tex | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index aea2bae38d..6a8bda35d6 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -947,6 +947,14 @@ time of writing this documentation, the default value is 50).
 \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}}
 This command displays the current nesting depth used for display.
 
+\subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
+This command enables the printing of the ``{\tt (dependent evars: \ldots)}''
+line when {\tt -emacs} is passed.
+
+\subsection[\tt Unset Printing Dependent Evars Line.]{\tt Unset Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
+This command disables the printing of the ``{\tt (dependent evars: \ldots)}''
+line when {\tt -emacs} is passed.
+
 %\subsection{\tt Abstraction ...}
 %Not yet documented.
 
-- 
cgit v1.2.3