aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
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 {} \;
###########################################################################