diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-27 16:02:55 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-27 16:02:55 +0000 |
| commit | 69af9a48257685132faa55d28cc8751b5e4acf11 (patch) | |
| tree | 1d4b9e9f701cfa34b1f4058753a763dcaea167ae /doc/refman | |
| parent | d9e885515da1592075f5599290e6117c095216b4 (diff) | |
Ajout de la doc de l'option -stdout de coqdoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8749 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman')
| -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 7862c5c38..f2630da07 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 |