From dbfa2fa4b310f612c47807eeecc6b8ae5f42eaab Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Tue, 23 Feb 1999 10:26:40 +0000
Subject: extended section on Coq tags

---
 doc/ProofGeneral.texi | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 755e009e..03f0644a 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1936,7 +1936,8 @@ the @code{Search} command of Coq.
 @c could be generic
 
 Coq Proof General provides the program @file{coqtags} to generate tags
-for Coq proof scripts.  
+for Coq proof scripts. Invoking @samp{coqtags *.v} produces a file
+@file{TAGS} for all files @samp{*.v} in the current directory.
 
 See @ref{Support for tags} for further details on tags.
 
-- 
cgit v1.2.3