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/output.ml | |
parent | 3e5505719ca9689a01f2b5c53e275e80201c64c4 (diff) |
Coq_makefile.generate_conf_coq_config: remove unused argument.
Diffstat (limited to 'tools/coqdoc/output.ml')
0 files changed, 0 insertions, 0 deletions