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

[Hauke Mehrtens]

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 at hauke-m.de>
---
 github-merge-pr.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
2.45.2