[NEW] Adds offer to push to origin/main

msageryd · Jul 13, 2023 · 66257bb · 66257bb
1 parent 35630a8
commit 66257bb
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/bin/tag-release.fish b/bin/tag-release.fish
@@ -103,5 +103,9 @@ allow_or_exit "Now merging branch '$git_branch' into 'main' …"
 git checkout main
 git pull --tags
 git merge -m "[MRG] Merges release '$release_tag'" --no-edit --no-ff $git_branch
+
+allow_or_exit "Push main to remote?"
+git push
+
 echo "Done!"
 echo