From 12e9483c80b673522226fc0fa82a6e085a14d366 Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 7 Jan 2009 19:07:19 +0000
Subject: Fix build for git users

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11760 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build | 8 ++++----
 1 file 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; \
-- 
cgit v1.2.3