aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-12-19 15:18:19 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-12-19 15:18:19 +0000
commita499d23cb1e35b58c8fd4c6f8851444ee09739cf (patch)
tree8dd606330a6a367941391e00e906f7169e77adc3
parenta32ce58114fabbd53447dca00e7f0c12990f4f17 (diff)
Adaptation à Subversion 1.4
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9457 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile7
1 files changed, 5 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index aabf09f0f..a0e1fbd90 100644
--- a/Makefile
+++ b/Makefile
@@ -1596,8 +1596,11 @@ parsing/lexer.cmo: parsing/lexer.ml4
revision:
ifeq ($(CHECKEDOUT),1)
- /bin/rm -f revision
- sed -ne '/url/s/^.*\/\([^\/]\{1,\}\)"$$/\1/p' .svn/entries > revision
- sed -ne '/revision/s/^.*"\([0-9]\{1,\}\)".*$$/r\1/p' .svn/entries >> revision
+ if test -x `which svn`; then \
+ export LANG=C; \
+ svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision; \
+ svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision; \
+ fi
endif
archclean::