aboutsummaryrefslogtreecommitdiff
path: root/test-suite/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile3
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