summaryrefslogtreecommitdiff
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2014-01-19 15:09:23 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2014-01-19 15:09:23 +0100
commitd2c5c5e616a6e118291fe1ce9965c731adac03a8 (patch)
tree7b000ad50dcc45ff1c63768a983cded1e23a07ca /tools/coqdep.ml
parentdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (diff)
Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r--tools/coqdep.ml13
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 ()