github-merge-pr: Add option to ignore .mergeable

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>

diff --git a/github-merge-pr.sh b/github-merge-pr.sh
index 76aec20b73d941aa69c9803d1d0d5236ce51a70f..f294c850c963ed35f80dc21bb8eca9a632d0c62e 100755 (executable)
--- 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