[maintainer-tools PATCH 0/4] github-merge-pr: Misc patches

[Hauke Mehrtens]

This adds support for my use case. ;-)

I want to do the operations which are affecting the remote manually.
Sometimes I am doing manual changes in between before merging the PR.

Hauke Mehrtens (4):
  github-merge-pr: Use GITHUB_TOKEN for API access
  github-merge-pr: Add option for no remote operations
  github-merge-pr: Add option to ignore .mergeable
  github-merge-pr: doc: Install extra git-filter-repo

 github-merge-pr.sh | 27 +++++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

-- 
2.45.2