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 | |
| parent | 198bf0a3cf310ef37a8bd561ad6fa5f67dfc6ebd (diff) | |
| parent | dddcd01010cbd6c1df1832b5069492d95880d5e5 (diff) | |
Merge PR #9998: coq_makefile: do not pass -opt/-byte to coqc (fix #9974)
Reviewed-by: ejgallego
| -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) |