diff options
| author |  Gregory Malecha <gmalecha@cs.harvard.edu> | 2014-05-10 00:47:16 -0400 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-05-26 13:37:36 +0200 |
| commit | 13deafee96893a5ec332ad221469e3e5460693f1 (patch) | |
| tree | c33a858cee5305f75b5d67f24724e7aa2e085a87 /tools/coqdep.ml | |
| parent | 525094414bf74445f930e170a823a49107726f6f (diff) | |
make coqdep canonicalize paths from the command line
- logical paths given to -R and -I should be split
on periods.
- it also seems like giving an empty string should
result in the empty path rather than the singleton
path with an empty string as an identifier.
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 1517121bf..febde9b69 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -439,6 +439,8 @@ let usage () = eprintf " -dumpgraph f : print a dot dependency graph in file 'f'\n"; exit 1 +let split_period = Str.split (Str.regexp (Str.quote ".")) + let rec parse = function | "-c" :: ll -> option_c := true; parse ll | "-D" :: ll -> option_D := true; parse ll @@ -446,13 +448,13 @@ let rec parse = function | "-boot" :: ll -> Flags.boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll - | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r [ln]; parse ll + | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r (split_period ln); parse ll | "-I" :: r :: "-as" :: [] -> usage () | "-I" :: r :: ll -> add_dir add_known r []; parse ll | "-I" :: [] -> usage () - | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll + | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll | "-R" :: r :: "-as" :: [] -> usage () - | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll + | "-R" :: r :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll | "-R" :: ([] | [_]) -> usage () | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll |