aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaxime Dénès2018-11-27 08:49:45 +0100
committerMaxime Dénès2018-12-12 12:25:52 +0100
commitce0924599497800773ebc95b392e678926ea1820 (patch)
treeebb84815c8d88c282b3f554fd8ff91b5382c7125
parent84a950c8e1fa06d0dd764e9a426edbd987a7989e (diff)
User flags for coqtop/coqc in Makefile and CI build template
-rw-r--r--Makefile.build5
1 files changed, 4 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build
index ec9b81dba4..0a73562467 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -44,6 +44,9 @@ NO_RECALC_DEPS ?=
# Non-empty runs the checker on all produced .vo files:
VALIDATE ?=
+# When non-empty, passed as extra arguments to coqtop/coqc:
+COQUSERFLAGS ?=
+
# Output file names for timed builds
TIME_OF_BUILD_FILE ?= time-of-build.log
TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log
@@ -191,7 +194,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
# the output format of the unix command time. For instance:
# TIME="%C (%U user, %S sys, %e total, %M maxres)"
-COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR)
+COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS)
BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS))