From 391372193c2a5170f9c14fc82a8a9336419a9f76 Mon Sep 17 00:00:00 2001
From: Ben Gras <ben@minix3.org>
Date: Thu, 6 Oct 2011 19:10:49 +0000
Subject: [PATCH] release: by default leave src/.git

	. facilitates easy updates of installs
	. removal can be restored with release.sh -m
---
 tools/release.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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