diff options
| author | Emilio Jesus Gallego Arias | 2019-04-26 14:34:17 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-26 14:34:17 +0200 |
| commit | ae4239d6a5f4afcd9b7321dba790ffd4a64994a1 (patch) | |
| tree | 0b98f5ba9ad4b7defb9bcf1551a25baff99110e0 /Makefile.doc | |
| parent | 198bf0a3cf310ef37a8bd561ad6fa5f67dfc6ebd (diff) | |
| parent | dddcd01010cbd6c1df1832b5069492d95880d5e5 (diff) | |
Merge PR #9998: coq_makefile: do not pass -opt/-byte to coqc (fix #9974)
Reviewed-by: ejgallego
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions