diff mbox series

[maintainer-tools,2/4] github-merge-pr: Add option for no remote operations

Message ID 20240706160725.3257906-3-hauke@hauke-m.de
State Accepted
Delegated to: Hauke Mehrtens
Headers show
Series github-merge-pr: Misc patches | expand

Commit Message

Hauke Mehrtens July 6, 2024, 4:07 p.m. UTC 
This adds the new option GITHUB_NO_PUSH which will prevent the script
from doing any changes to remote repositories.

Signed-off-by: Hauke Mehrtens <hauke@hauke-m.de>
---
 github-merge-pr.sh | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
diff mbox series

Patch

diff --git a/github-merge-pr.sh b/github-merge-pr.sh
index db49c92..76aec20 100755
--- a/github-merge-pr.sh
+++ b/github-merge-pr.sh
@@ -158,6 +158,21 @@  if [ "$(echo "$PR_INFO" | jq -r ".maintainer_can_modify")" == "true" ]; then
 		exit 9
 	fi
 
+	if [ "$GITHUB_NO_PUSH" = "1" ]; then
+		echo "next commands:"
+		if [ "$(echo "$PR_INFO" | jq -r ".maintainer_can_modify")" == "true" ]; then
+			echo "$GIT push $PR_USER HEAD:$PR_BRANCH --force"
+			echo "$GIT checkout $BRANCH"
+			echo "$GIT merge --ff-only $PR_USER/$PR_BRANCH"
+		else
+			echo "$GIT checkout $BRANCH"
+			echo "$GIT merge --ff-only $LOCAL_PR_BRANCH"
+		fi
+		echo "$GIT push"
+		echo "$GIT branch -D $LOCAL_PR_BRANCH"
+		exit 20
+	fi
+
 	echo "Force pushing $LOCAL_PR_BRANCH to HEAD:$PR_BRANCH for $PR_USER"
 	if ! $GIT push $PR_USER HEAD:$PR_BRANCH --force; then
 		echo "Failed to force push HEAD to $PR_USER" >&2