Hi, Do you have any objections to this? If nobody objects this, I'll merge this in next week.
Thanks, -- kou In <20220518.124328.1547483441605263532....@clear-code.com> "Merge a pull request with GitHub API" on Wed, 18 May 2022 12:43:28 +0900 (JST), Sutou Kouhei <k...@clear-code.com> wrote: > Hi, > > How about using GitHub API instead of local "git merge" to > merge a pull request? > > > 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. > > > See also: > > * https://issues.apache.org/jira/browse/ARROW-16602 > * https://github.com/apache/arrow/pull/13184 > > > Thanks, > -- > kou
