diff --git a/tools/release.sh b/tools/release.sh index 74905cd59..c01b5eed7 100755 --- a/tools/release.sh +++ b/tools/release.sh @@ -205,7 +205,9 @@ then else REVTAG=`(cd $srcdir && git show-ref HEAD -s10)` echo "Retrieved repository head is $REVTAG." fi - rm -r $srcdir/.git + if [ $MINIMAL -ne 0 ] + then rm -r $srcdir/.git + fi echo " /* Added by release script */ #ifndef _VCS_REVISION