From d25ded6d3d61daac4e32fec377033143be4d8449 Mon Sep 17 00:00:00 2001
From: Ben Gras <ben@minix3.org>
Date: Tue, 21 Feb 2012 01:20:00 +0100
Subject: [PATCH] fix for git commit id from branch

	. git would take remote repo HEAD otherwise
---
 tools/release.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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
-- 
2.44.0