From 8a03b56c47ed0d216f797fefd531286d6b74a3fb Mon Sep 17 00:00:00 2001
From: notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 11 Oct 2006 13:04:47 +0000
Subject: Ajout d'une option -annotate au configure+ changement du comportement
 par défaut de make
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9232 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 config/Makefile.template | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

(limited to 'config')

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
 
-- 
cgit v1.2.3