[ARROW-16602] [Dev] Use GitHub API to merge pull request

• Type: Improvement
• Status: Resolved
• Priority: Major
• Resolution: Fixed
• Fix Version/s: 9.0.0
• Component/s: Developer Tools
• Labels: pull-request-available
• External issue URL: https://github.com/apache/arrow/issues/31956
• Assignee: Kouhei Sutou
• Reporter: Kouhei Sutou
• Created: 18/May/22 03:37
• Updated: 11/Jan/23 11:45
• Resolved: 31/May/22 21:01

Description

We use local "git merge" to merge a pull request in dev/merge_arrow_pr.py.

If we use "git merge" to merge a pull request, GitHub's Web UI shows "Closed" mark not "Merged" mark in a pull request page. This sometimes confuses new contributors. "Why was my pull request closed without merging?" See https://github.com/apache/arrow/pull/12004#issuecomment-1031619771 for example.

If we use GitHub API https://docs.github.com/en/rest/pulls/pulls#merge-a-pull-request to merge a pull request, GitHub's Web UI shows "Merged" mark not "Closed" mark. See https://github.com/apache/arrow/pull/13180 for example. I used GitHub API to merge the pull request.

And we don't need to create a local branch on local repository to merge a pull request. But we must specify ARROW_GITHUB_API_TOKEN to run dev/merge_arrow_pr.py.

Issue Links

• supercedes: ARROW-13664 [Developer] Append better merge visibility to merge_arrow_pr.py
• links to: GitHub Pull Request #13184