release: by default leave src/.git

	. facilitates easy updates of installs
	. removal can be restored with release.sh -m

diff --git a/tools/release.sh b/tools/release.sh
index 74905cd592c389359a0510c8b78531cc9204ea06..c01b5eed7fc80ce84535a17c2583860227ea7627 100755 (executable)
--- 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