diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-06 15:08:08 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-06 15:08:08 +0100 |
| commit | 6599e31f04b6e8980de72e9d3913b70c04b6698c (patch) | |
| tree | f28177b60a7f537bde0f4763c320e08529bddbb3 /tools/coqdep.ml | |
| parent | d0d46d9c5a93de25ecf0202a0ab3dbd83f1ed693 (diff) | |
Remove deprecated command-line options such as "-as".
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index aacfccfd7..0634f97fa 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -444,15 +444,8 @@ let rec parse = function | "-boot" :: ll -> option_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_rec_dir_no_import add_known r []; - add_rec_dir_no_import add_known r (split_period ln); - parse ll - | "-I" :: r :: "-as" :: [] -> usage () | "-I" :: r :: ll -> add_caml_dir r; parse ll | "-I" :: [] -> usage () - | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll - | "-R" :: r :: "-as" :: [] -> usage () | "-R" :: r :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll | "-Q" :: r :: ln :: ll -> add_rec_dir_no_import add_known r (split_period ln); parse ll | "-R" :: ([] | [_]) -> usage () |