diff mbox series

[maintainer-tools,3/4] github-merge-pr: Add option to ignore .mergeable

Message ID 20240706160725.3257906-4-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 
The option IGNORE_MERGEABLE allows to ignore if the PR is mergeable.
This allows to prepare PRs which can not be force pushed with this
script.

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

Patch

diff --git a/github-merge-pr.sh b/github-merge-pr.sh
index 76aec20..f294c85 100755
--- a/github-merge-pr.sh
+++ b/github-merge-pr.sh
@@ -123,7 +123,7 @@  fi
 echo "Fetching remote $PR_USER"
 $GIT fetch $PR_USER $PR_BRANCH
 
-if [ "$(echo "$PR_INFO" | jq -r ".maintainer_can_modify")" == "true" ]; then
+if [ "$(echo "$PR_INFO" | jq -r ".maintainer_can_modify")" == "true" ] || [ "$IGNORE_MERGEABLE" = "1" ]; then
 	echo "Creating branch $LOCAL_PR_BRANCH for $PR_BRANCH"
 	if ! $GIT checkout -b $LOCAL_PR_BRANCH $PR_USER/$PR_BRANCH; then
 		echo "Failed to checkout new branch $PR_BRANCH from $PR_USER/$PR_BRANCH" >&2