aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-08-28 22:39:41 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-08-28 22:39:41 +0200
commit23a129e18ae930de5f40df59307c48c68d62d8d7 (patch)
tree403387a98ea9da32d70ac5b5607d5be30fa0ee42 /Makefile
parent780ad9d001af651a49d7470e963ed9a49ee11a4c (diff)
parent192bd462233d0284fa3d5f8e8994a514b549713e (diff)
downloadcompcert-kvx-23a129e18ae930de5f40df59307c48c68d62d8d7.tar.gz
compcert-kvx-23a129e18ae930de5f40df59307c48c68d62d8d7.zip
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 4f9b53a2..aa99786b 100644
--- a/Makefile
+++ b/Makefile
@@ -32,6 +32,7 @@ RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \
COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) $(subst /,.,compcert.$(d)))
+COQCOPTS ?= -w -undeclared-scope
COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
COQDOC="$(COQBIN)coqdoc"