option aggressive (pas testee)

git_update.sh

@@ -39,6 +39,9 @@ usage[H]="Use real home dir"
 varia[H]=use_home
 use_home=false
 
+usage[a]="use git clean with the aggressive option"
+varia[a]=be_aggressive
+be_aggressive=false
 
 . driglibash-args
 
@@ -79,7 +82,11 @@ if [ -d .git ] ; then
 	run git fetch --tags --depth=1 --prune --prune-tags origin $ref
 	run git reset --hard FETCH_HEAD 
 	git reflog expire --expire=now --all 
-	git gc --aggressive --prune=now
+	if "$be_aggressive" ; then
+		git gc --prune=now --aggressive
+	else
+		git gc --prune=now
+	fi
 	# Preserve existing files in some cases
 	if ! "$nonempty_target" ; then #so we keep uncommitted files when not in -N
 		git clean -qffdx