github-merge-pr: Add option to ignore .mergeable
authorHauke Mehrtens <hauke@hauke-m.de>
Sat, 6 Jul 2024 16:07:24 +0000 (18:07 +0200)
committerChristian Marangi <ansuelsmth@gmail.com>
Tue, 16 Jul 2024 17:09:37 +0000 (19:09 +0200)
commitbed63ed659a61bab5cc046d8ac8c8774b294f0e6
tree7267e613e443353d892affc0152893f90c1c3204
parentb5d78394fc963606f935999688a40bd52504415e
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>
github-merge-pr.sh