retag.sh: Add separate push command prior to tags push

JOJ0 · Jan 25, 2022 · 1232f91 · 1232f91
1 parent 70f1a84
commit 1232f91
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/retag.sh b/retag.sh
@@ -9,4 +9,4 @@ PUSH_OPTS="$2"
 set -x
 VERS=$1
 
-git tag -d $VERS; git push origin --delete $VERS; git tag $VERS; git push --tags --follow-tags
+git tag -d $VERS; git push origin --delete $VERS; git tag $VERS; git push; git push --tags --follow-tags