diff options
| author | Enrico Tassi | 2019-04-25 13:44:40 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-04-25 13:44:40 +0200 |
| commit | dddcd01010cbd6c1df1832b5069492d95880d5e5 (patch) | |
| tree | 7afe86e1c8ee026f2a5e4dd44e5b7e7204479d81 /plugins/funind/plugin_base.dune | |
| parent | 47f202605b4ef1795a31312b3ff2eda006fa46a6 (diff) | |
coq_makefile: do not pass -opt/-byte to coqc (fix #9974)
Diffstat (limited to 'plugins/funind/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions