aboutsummaryrefslogtreecommitdiffhomepage
path: root/config/Makefile.template
diff options
context:
space:
mode:
Diffstat (limited to 'config/Makefile.template')
-rw-r--r--config/Makefile.template15
1 files changed, 3 insertions, 12 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index 5310aec94..a3465722f 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -61,6 +61,9 @@ CAMLLINK="BYTECAMLC"
CAMLOPTLINK="NATIVECAMLC"
CAMLMKTOP="CAMLMKTOPEXEC"
+# Caml flags
+CAMLFLAGS=CAMLANNOTATEFLAG
+
# Compilation debug flag
CAMLDEBUG=COQDEBUGFLAG
@@ -125,18 +128,6 @@ HASCOQIDE=COQIDEOPT
# Defining REVISION
CHECKEDOUT=CHECKEDOUTSOURCETREE
-.PHONY: revision
-
-revision:
-ifeq ($(CHECKEDOUT),1)
- - /bin/rm -f revision
- sed -ne '/url/s/^.*\/\([^\/]\+\)"$$/\1/p' .svn/entries > revision
- sed -ne '/revision/s/^.*"\([0-9]\+\)".*$$/r\1/p' .svn/entries >> revision
-endif
-
-archclean::
- /bin/rm -f revision
-
# make or sed are bogus and believe lines not terminating by a return
# are inexistent