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 9616f50512e1118c56590f5baadd13a57d1d5293..fb7582e91aee174be11fc595b76828717a262c30 100755 (executable)
--- 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