aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-01-07 19:07:19 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-01-07 19:07:19 +0000
commit12e9483c80b673522226fc0fa82a6e085a14d366 (patch)
tree28b7becd0e3f6d1173d3a50533391f5c7e1aab37
parent7534c1c085b2bd066f44d87c3caeb317e93d224c (diff)
Fix build for git users
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11760 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.build8
1 files changed, 4 insertions, 4 deletions
diff --git a/Makefile.build b/Makefile.build
index 908213d42..214095b5f 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -804,14 +804,14 @@ ifeq ($(CHECKEDOUT),gnuarch)
fi
endif
ifeq ($(CHECKEDOUT),git)
- $(HIDE)set -e; \
+ $(HIDE)set -e; \
if test -x "`which git`"; then \
LANG=C; export LANG; \
- GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/let version = "\1"/p'); \
+ GIT_BRANCH=$$(git branch -a | sed -ne 's/^\* //p'); \
GIT_HOST=$$(hostname --fqdn); \
GIT_PATH=$$(pwd); \
- (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \
- git log -1 | sed -ne '/^commit /s/^commit[[:space:]]\+\(.*\)/let revision = "\1"/p' >> revision.new; \
+ echo "let version = \"$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}\"" > revision.new; \
+ echo "let revision = \"$$(git show-ref $${GIT_BRANCH}|sed -ne 's/ .*//p')\"" >> revision.new; \
fi
endif
$(HIDE)set -e; \