aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2005-11-05 19:36:08 +0000
committerherbelin2005-11-05 19:36:08 +0000
commit8b706d84bb2c158e9df3fd17e278f6ba3769a277 (patch)
tree7e36c08688eda6257cc5d392fc6fb1c29c2aa3bd
parent1e4f6821715afce4b08b384a70fae5d7d9c7aad3 (diff)
option -w y finalement pas admise par ocamlc <= 3.08.2
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7519 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 9daaeea4a4..ca3d88a983 100644
--- a/Makefile
+++ b/Makefile
@@ -77,8 +77,8 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
-BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) -w y
-OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -w y -noassert
+BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG)
+OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -noassert
OCAMLDEP=ocamldep
DEPFLAGS=$(LOCALINCLUDES)