From: Ben Gras <ben@minix3.org>
Date: Tue, 21 Feb 2012 00:20:00 +0000 (+0100)
Subject: fix for git commit id from branch
X-Git-Tag: v3.2.1~704
X-Git-Url: http://zhaoyanbai.com/repos//%22https:/www.google.com/jsapi/%22?a=commitdiff_plain;h=d25ded6d3d61daac4e32fec377033143be4d8449;p=minix.git

fix for git commit id from branch

	. git would take remote repo HEAD otherwise
---

diff --git a/tools/release.sh b/tools/release.sh
index 9616f5051..fb7582e91 100755
--- a/tools/release.sh
+++ b/tools/release.sh
@@ -206,8 +206,8 @@ then
 	if [ "$REVTAG" ]
 	then	echo "Doing checkout of $REVTAG."
 		(cd $srcdir && git checkout $REVTAG )
-	else	REVTAG=`(cd $srcdir && git show-ref HEAD -s10)`
-		echo "Retrieved repository head is $REVTAG."
+	else	REVTAG=`(cd $srcdir && git rev-parse --short HEAD)`
+		echo "Retrieved repository head in $srcdir is $REVTAG."
 	fi
 	if [ $MINIMAL -ne 0 ]
 	then	rm -r $srcdir/.git