diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-07 19:07:19 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-07 19:07:19 +0000 |
commit | 12e9483c80b673522226fc0fa82a6e085a14d366 (patch) | |
tree | 28b7becd0e3f6d1173d3a50533391f5c7e1aab37 | |
parent | 7534c1c085b2bd066f44d87c3caeb317e93d224c (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.build | 8 |
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; \ |