aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-07-28 18:05:39 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-07-28 18:05:39 +0000
commit7e13b8a0627c09a49487dc64210fa4616cffc66c (patch)
treeb44dee28523fd5f63edde51c15571d69251ab221 /config
parent5ce1ece6393b33a213dfba2e3b63a130e398d84f (diff)
Modifications dans les scripts de configuration (coqtop et coqide affichent maintenant le numéro de révision svn) + correction problème OCaml 3.07 et caml_;odify
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9063 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'config')
-rw-r--r--config/Makefile.template16
1 files changed, 16 insertions, 0 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index aa7f2d621..d5c2a1436 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -113,5 +113,21 @@ REALS=REALSOPT
# CoqIde (no/byte/opt)
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
+