[Dev] Use GitHub API to merge pull request

[asfimport]

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 #12004 (comment) 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 #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.

Reporter: Kouhei Sutou / @kou
Assignee: Kouhei Sutou / @kou
Watchers: Rok Mihevc / @rok

Related issues:

• [Developer] Append better merge visibility to merge_arrow_pr.py (supercedes)

PRs and other links:

• GitHub Pull Request #13184

_{Note: This issue was originally created as ARROW-16602. Please see the migration documentation for further details.}

[asfimport]

Kouhei Sutou / @kou:
Issue resolved by pull request 13184
#13184