diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-31 16:01:11 +0200 |
|---|---|---|
| committer |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-03 13:36:05 +0200 |
| commit | b1b89157a7ab59278db1fed77f41cab2aa2d3a9f (patch) | |
| tree | fb8a869c5a23c0b6392f35fa9178add3a46bf044 /tools/coqdoc/index.mli | |
| parent | 3e5505719ca9689a01f2b5c53e275e80201c64c4 (diff) | |
Coq_makefile.generate_conf_coq_config: remove unused argument.
Diffstat (limited to 'tools/coqdoc/index.mli')
0 files changed, 0 insertions, 0 deletions