diff options
| author | Emilio Jesus Gallego Arias | 2020-02-13 00:24:58 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-13 22:11:05 +0100 |
| commit | 4ea2825a4589b0c77225dd6f4caf98b12ac6dd6f (patch) | |
| tree | bff1d2d38f7e8dbc6f55506e8bcc1e8fc7821948 /tools/coqdep.ml | |
| parent | 2e36df827c85ea93cc7614dc25f82a16f72e6e9d (diff) | |
[coqdep] Merge `-sort` and `-suffix` options.
They are always used together, no other use case of `-suffix` that I
can see.
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 950c784325..23cc83b8d3 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -44,7 +44,6 @@ let usage () = eprintf " -vos : also output dependencies about .vos files\n"; eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; eprintf " -coqlib dir : set the coq standard library directory\n"; - eprintf " -suffix s : \n"; eprintf " -slash : deprecated, no effect\n"; eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n"; exit 1 @@ -81,8 +80,6 @@ let rec parse = function | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll | "-coqlib" :: [] -> usage () - | "-suffix" :: s :: ll -> suffixe := s ; parse ll - | "-suffix" :: [] -> usage () | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll |