diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /tools/coqdoc/main.ml | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'tools/coqdoc/main.ml')
-rw-r--r-- | tools/coqdoc/main.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 9531cd2b..22febd6a 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -61,8 +61,8 @@ let usage () = prerr_endline " --coqlib_path <dir> set the path where Coq files are installed"; prerr_endline " -R <dir> <coqdir> map physical dir to Coq dir"; prerr_endline " -Q <dir> <coqdir> map physical dir to Coq dir"; - prerr_endline " --latin1 set ISO-8859-1 input language"; - prerr_endline " --utf8 set UTF-8 input language"; + prerr_endline " --latin1 set ISO-8859-1 mode"; + prerr_endline " --utf8 set UTF-8 mode"; prerr_endline " --charset <string> set HTML charset"; prerr_endline " --inputenc <string> set LaTeX input encoding"; prerr_endline " --interpolate try to typeset identifiers in comments using definitions in the same module"; @@ -557,10 +557,8 @@ let produce_output fl = (*s \textbf{Main program.} Print the banner, parse the command line, read the files and then call [produce_document] from module [Web]. *) -let main () = +let _ = let files = parse () in Index.init_coqlib_library (); if not !quiet then banner (); if files <> [] then produce_output files - -let _ = Printexc.catch main () |