diff options
| -rw-r--r-- | tools/coqdoc/main.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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"; |