diff options
Diffstat (limited to 'doc/RefMan-com.tex')
| -rwxr-xr-x | doc/RefMan-com.tex | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex index 34e4211493..cf5b100e7f 100755 --- a/doc/RefMan-com.tex +++ b/doc/RefMan-com.tex @@ -185,6 +185,11 @@ The following command-line options are recognized by the commands {\tt Switch on the debug flag. +\item[{\tt -xml}]\ + + This option is for use with {\tt coqc}. It tells \Coq\ to export on + the standard output the content of the compiled file into XML format. + \item[{\tt -emacs}]\ Tells \Coq\ it is executed under Emacs. |