diff options
| author | Enrico Tassi | 2020-03-20 14:26:48 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-03-20 14:26:48 +0100 |
| commit | 5b7a6471cf812a708dbbb8943f30d525e46250f6 (patch) | |
| tree | caf236823940843f1609112162801250bf5dfdb6 /test-suite/Makefile | |
| parent | 06b820259989a59080d0dc68bf0c633994fe221f (diff) | |
| parent | 57bc1b7921da4ae54ee5d3b999351f297556fd65 (diff) | |
Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yes
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index aca7ab0b28..6696f1431e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -49,7 +49,8 @@ endif endif # exists ../_build export COQLIB -COQFLAGS?= +COQEXTRAFLAGS?= +COQFLAGS?=$(COQEXTRAFLAGS) coqc := $(BIN)coqc -q -R prerequisite TestSuite $(COQFLAGS) coqchk := $(BIN)coqchk -R prerequisite TestSuite |