aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authornotin2006-11-16 11:27:01 +0000
committernotin2006-11-16 11:27:01 +0000
commitb95b06d10ebfcf9c536c932ae6f4d8fe8c24f966 (patch)
treea761d168981209534d0a28ce84b7840c94ad1814 /Makefile
parent3bc4bde3c83333c1825b0f9c6c03474de12fb87e (diff)
Adaptation à FreeBSD
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9378 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index f4f0517864..1feac1659f 100644
--- a/Makefile
+++ b/Makefile
@@ -1595,8 +1595,8 @@ parsing/lexer.cmo: parsing/lexer.ml4
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
+ sed -ne '/url/s/^.*\/\([^\/]\{1,\}\)"$$/\1/p' .svn/entries > revision
+ sed -ne '/revision/s/^.*"\([0-9]\{1,\}\)".*$$/r\1/p' .svn/entries >> revision
endif
archclean::