aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-04-28 19:21:21 +0200
committerGaëtan Gilbert2019-04-28 19:21:21 +0200
commit02a98973d2bd1e6fd5f7489da718f5a313fc834c (patch)
treeb7e352aa4a0940e19bf858c451535bfb063572db /tools
parentae4239d6a5f4afcd9b7321dba790ffd4a64994a1 (diff)
parent728216337e2541b37135d86c1b0206706cf4ed1a (diff)
Merge PR #9605: [coq_makefile] Enforce warn_error for plugins.
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in5
1 files changed, 3 insertions, 2 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 51e0300182..2ec55d1bd0 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -38,6 +38,7 @@ DOCDIR := $(COQMF_DOCDIR)
OCAMLFIND := $(COQMF_OCAMLFIND)
CAMLFLAGS := $(COQMF_CAMLFLAGS)
HASNATDYNLINK := $(COQMF_HASNATDYNLINK)
+OCAMLWARN := $(COQMF_WARN)
@CONF_FILE@: @PROJECT_FILE@
@COQ_MAKEFILE_INVOCATION@
@@ -190,9 +191,9 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@
COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
-
# ocamldoc fails with unknown argument otherwise
-CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
+CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
+CAMLFLAGS+=$(OCAMLWARN)
ifneq (,$(TIMING))
TIMING_ARG=-time