aboutsummaryrefslogtreecommitdiff
path: root/test-suite/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile5
1 files changed, 3 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 34a1900bbc..37091a49e5 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -36,9 +36,10 @@ include ../Makefile.common
# easily overridden
LIB := ..
BIN := $(shell cd ..; pwd)/bin/
+COQFLAGS?=
-coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite
-coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
+coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite $(COQFLAGS)
+coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS)
coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
coqdoc := $(BIN)coqdoc
coqtopbyte := $(BIN)coqtop.byte