diff options
author | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
commit | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (patch) | |
tree | 7b000ad50dcc45ff1c63768a983cded1e23a07ca /tools/coqdep.ml | |
parent | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (diff) |
Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r-- | tools/coqdep.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 90cdd12d..8a5f0695 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -157,9 +157,10 @@ let declare_dependencies () = (List.rev !vAccu) let usage () = - eprintf - "[ usage: coqdep [-w] [-I dir] [-R dir coqdir] [-coqlib dir] [-c] [-i] [-D] <filename>+ ]\n"; - flush stderr; + eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-R dir coqdir] <filename>+\n"; + eprintf " extra options:\n"; + eprintf " -coqlib dir : set the coq standard library directory\n"; + eprintf " -exclude-dir f : skip subdirectories named f during -R search\n"; exit 1 let rec parse = function @@ -177,9 +178,11 @@ let rec parse = function | "-R" :: r :: "-as" :: [] -> usage () | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll | "-R" :: ([] | [_]) -> usage () - | "-coqlib" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll + | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll + | "-exclude-dir" :: [] -> usage () + | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () - | "-suffix" :: (s :: ll) -> suffixe := s ; parse ll + | "-suffix" :: s :: ll -> suffixe := s ; parse ll | "-suffix" :: [] -> usage () | "-slash" :: ll -> option_slash := true; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () |