aboutsummaryrefslogtreecommitdiff
path: root/Makefile.build
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build13
1 files changed, 8 insertions, 5 deletions
diff --git a/Makefile.build b/Makefile.build
index ec9b81dba4..34d7ce42f7 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))
@@ -572,11 +575,11 @@ module Gramext = Gramlib__Gramext \
module Grammar = Gramlib__Grammar" > $@
gramlib/.pack/gramlib__P%: gramlib/p% | gramlib/.pack
- cp -a $< $@
- sed -e "1i # 1 \"$<\"" -i $@
+ printf '# 1 "%s"\n' $< > $@
+ cat $< >> $@
gramlib/.pack/gramlib__G%: gramlib/g% | gramlib/.pack
- cp -a $< $@
- sed -e "1i # 1 \"$<\"" -i $@
+ printf '# 1 "%s"\n' $< > $@
+ cat $< >> $@
# Specific rules for gramlib to pack it Dune / OCaml 4.08 style
GRAMOBJS=$(addsuffix .cmo, $(GRAMFILES))