Merge topic 'update-gitsetup'

631da93 Merge branch 'upstream-GitSetup' into update-gitsetup 8a0f726 GitSetup 2017-10-26 (1639317d) Acked-by: Kitware Robot <[email protected]> Acked-by: Ben Boeckel <[email protected]> Merge-request: !3623
leftwillow · Nov 27, 2017 · c89be39 · c89be39
2 parents 20d3125 + 631da93
commit c89be39
Showing 1 changed file with 10 additions and 2 deletions.
diff --git a/Utilities/GitSetup/git-gitlab-push b/Utilities/GitSetup/git-gitlab-push
@@ -23,7 +23,8 @@ OPTIONS
     Show what would be pushed without actually updating the destination
 
 -f,--force
-    Force-push the topic HEAD to rewrite the destination branch
+    Force-push the topic HEAD to rewrite the destination branch (use twice
+    to ignore stale remote tracking branches)
 
 --keep-data
     Do not erase local data refs after pushing
@@ -117,7 +118,14 @@ set_upstream=true
 # Parse the command line options.
 while test $# != 0; do
 	case "$1" in
-		-f|--force)    force='+'; lease=true ;;
+		-f|--force)
+			if test -n "$force"; then
+				lease=false
+			else
+				lease=true
+			fi
+			force='+'
+			;;
 		--keep-data)   keep_data=1 ;;
 		--no-topic)    no_topic=1; set_upstream=false ;;
 		--no-data)     no_data=1 ;;