aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-04-06 16:01:44 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-04-06 16:01:44 +0200
commit4f8ba5f0651eb986a63ffc58c072ed06fac0f53b (patch)
tree76b8380685e31b59ab6134fd14e42cce4a15daa9 /Makefile
parent41b17255f3517b875c19cb7b5c340b88f77da920 (diff)
downloadcompcert-4f8ba5f0651eb986a63ffc58c072ed06fac0f53b.tar.gz
compcert-4f8ba5f0651eb986a63ffc58c072ed06fac0f53b.zip
Also enable warnings for doc generator.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 7df9e73f..4cc83f89 100644
--- a/Makefile
+++ b/Makefile
@@ -166,7 +166,7 @@ documentation: doc/coq2html $(FILES)
cp doc/coq2html.css doc/coq2html.js doc/html/
doc/coq2html: doc/coq2html.ml
- ocamlopt -o doc/coq2html str.cmxa doc/coq2html.ml
+ ocamlopt -w +a-29 -o doc/coq2html str.cmxa doc/coq2html.ml
doc/coq2html.ml: doc/coq2html.mll
ocamllex -q doc/coq2html.mll
@@ -262,7 +262,7 @@ check-admitted: $(FILES)
# UnionFind.UF.elt gives "Anomaly: Uncaught exception Reduction.NotConvertible"
check-proof: $(FILES)
- $(COQCHK) -admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind Complements
+ $(COQCHK) -admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind Complements
print-includes:
@echo $(COQINCLUDES)