From e8587d7875a0fb1d46541932231602e2326f3492 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 Jan 2004 16:49:26 +0000
Subject: Ajout option -xml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8478 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-com.tex | 5 +++++
 1 file changed, 5 insertions(+)

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.
-- 
cgit v1.2.3