aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authornotin2006-05-04 13:25:52 +0000
committernotin2006-05-04 13:25:52 +0000
commitbf962b3fae1f3ac8eb2170fb8d33fb004c3445fa (patch)
treea4ab685c48930918e2419e328156ba4761760d8f /Makefile
parentc3ac3f3a350ad96f9f9f9c22a516f84cf6ad193d (diff)
- intégration de la modification suggérée par L. Mamane: coqmktop passe maintenant aussi l'option -dtypes à ocamlmktop
- ajout d'une variable USERFLAGS, permettant à un utilisateur de rajouter facilement des options de compilation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8787 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile5
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index fd8e52c83a..45ae6c8c98 100644
--- a/Makefile
+++ b/Makefile
@@ -73,8 +73,8 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
-BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG)
-OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -noassert
+BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
+OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) $(USERFLAGS) -noassert
OCAMLDEP=ocamldep
DEPFLAGS=$(LOCALINCLUDES)
@@ -1696,5 +1696,6 @@ devel:
clean::
find . -name "\.#*" -exec rm -f {} \;
find . -name "*~" -exec rm -f {} \;
+ find . -name "*.annot" -exec rm -f {} \;
###########################################################################