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 /Makefile.build | |
| parent | fe6d6e9ab1291a03e5fe68287b90ee1b244e8f2d (diff) | |
[coqdep] Remove deprecated -slash , unused, undocumented -mldep option.
Diffstat (limited to 'Makefile.build')
0 files changed, 0 insertions, 0 deletions