diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /tools/coqdoc/main.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'tools/coqdoc/main.ml')
-rw-r--r-- | tools/coqdoc/main.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 59d1ac87..9531cd2b 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -60,6 +60,7 @@ let usage () = prerr_endline " --boot run in boot mode"; 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 " --charset <string> set HTML charset"; @@ -320,6 +321,10 @@ let parse () = add_path path log; parse_rec rem | "-R" :: ([] | [_]) -> usage () + | "-Q" :: path :: log :: rem -> + add_path path log; parse_rec rem + | "-Q" :: ([] | [_]) -> + usage () | ("-glob-from" | "--glob-from") :: f :: rem -> glob_source := GlobFile f; parse_rec rem | ("-glob-from" | "--glob-from") :: [] -> @@ -445,7 +450,7 @@ let gen_mult_files l = if (!header_trailer) then Output.trailer (); close_out_file() end - (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *) + (* NB: for latex and texmacs, a separated toc or index is meaningless... *) let read_glob_file vfile f = try Index.read_glob vfile f |