From c08932df65d65be39cd4ef7d7cb1b7012c4ec6f1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 13 Apr 2004 12:29:16 +0000
Subject: Suppression documentation option raw-comments qui est vraiment trop
 ad hoc pour l'export XML des .v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5669 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coqdoc/main.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 099eb6e0d6..9b9023438b 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -57,7 +57,6 @@ let usage () =
   prerr_endline "  --utf8              set UTF-8 input language";
   prerr_endline "  --charset <string>  set HTML charset";
   prerr_endline "  --inputenc <string> set LaTeX input encoding";
-  prerr_endline "  --raw-comments      don't insert comments in table";
   prerr_endline "";
   prerr_endline 
     "On-line documentation at http://www.lri.fr/~filliatr/coqdoc/\n";
-- 
cgit v1.2.3