diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-06-30 18:15:41 +0200 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-07-03 18:02:59 +0200 |
| commit | 157ccc2da0f62dad730f1f13b875c48e3af4eb09 (patch) | |
| tree | 77ea7cf4bfb4cdcba858ebc285419a58b3124cfb /tools/coqdoc | |
| parent | c892f8cab37c0a89f6975e6a14bebad4d86156bd (diff) | |
coqdoc is minimaly -Q aware
Diffstat (limited to 'tools/coqdoc')
| -rw-r--r-- | tools/coqdoc/main.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index b33ec1f03..88a102d85 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -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") :: [] -> |