diff options
| author | Emilio Jesus Gallego Arias | 2020-02-05 14:10:20 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-07 13:24:55 +0100 |
| commit | 9276876d66defa40adf0ff609c97150a6fe98d58 (patch) | |
| tree | ca04e463add013722777131b6962f5896fa4eb44 /tools/coqdep_common.mli | |
| parent | fe6d6e9ab1291a03e5fe68287b90ee1b244e8f2d (diff) | |
[coqdep] Remove deprecated -slash , unused, undocumented -mldep option.
Diffstat (limited to 'tools/coqdep_common.mli')
| -rw-r--r-- | tools/coqdep_common.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 6d49f7e06c..96266b8e36 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -30,7 +30,6 @@ val write_vos : bool ref type dynlink = Opt | Byte | Both | No | Variable val option_dynlink : dynlink ref -val option_mldep : string option ref val norec_dirs : StrSet.t ref val suffixe : string ref type dir = string option |