summaryrefslogtreecommitdiff
path: root/doc/refman/coqdoc.tex
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /doc/refman/coqdoc.tex
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'doc/refman/coqdoc.tex')
-rw-r--r--doc/refman/coqdoc.tex4
1 files changed, 4 insertions, 0 deletions
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