diff options
Diffstat (limited to 'doc/refman/coqdoc.tex')
| -rw-r--r-- | doc/refman/coqdoc.tex | 4 |
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 |