sanchayanmaity/minix
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

fix for git commit id from branch

Browse source 
. git would take remote repo HEAD otherwise
This commit is contained in:
Ben Gras 2012-02-21 01:20:00 +01:00
parent ee305598c5
commit d25ded6d3d
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tools/release.sh
View file

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