aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorherbelin2004-09-26 21:24:48 +0000
committerherbelin2004-09-26 21:24:48 +0000
commit50387c13a0a0384388adec0a674448b9ba270530 (patch)
tree2e39819648ec43b5a76392629024a8e12e05e8d9 /Makefile
parent648915221a74ba840334456ce68cf93295f9124d (diff)
no-assert en mode natif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6137 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 45d4b9b710..3c28da8faa 100644
--- a/Makefile
+++ b/Makefile
@@ -78,7 +78,7 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG)
-OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF)
+OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -noassert
OCAMLDEP=ocamldep
DEPFLAGS=$(LOCALINCLUDES)