From ce0924599497800773ebc95b392e678926ea1820 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 27 Nov 2018 08:49:45 +0100
Subject: User flags for coqtop/coqc in Makefile and CI build template

---
 Makefile.build | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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))
-- 
cgit v1.2.3