From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 doc/refman/coqdoc.tex | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'doc/refman/coqdoc.tex')

diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index 7862c5c3..f2630da0 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -264,6 +264,10 @@ suffix \verb!.tex!.
   
   Select a \texmacs\ output.
 
+\item[\texttt{--stdout}] ~\par
+
+  Write output to stdout.
+
 \item[\texttt{-o }\textit{file}, \texttt{\mm{}output }\textit{file}] ~\par
   
   Redirect the output into the file `\textit{file}' (meaningless with
-- 
cgit v1.2.3