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 /tools | |
| parent | 47f202605b4ef1795a31312b3ff2eda006fa46a6 (diff) | |
coq_makefile: do not pass -opt/-byte to coqc (fix #9974)
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 0236c549d5..51e0300182 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -176,7 +176,7 @@ COQCHKEXTRAFLAGS?= COQDOCEXTRAFLAGS?= # these flags do NOT contain the libraries, to make them easier to overwrite -COQFLAGS?=-q $(OPT) $(OTHERFLAGS) $(COQEXTRAFLAGS) +COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS) COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) |