Hi, There are no objections. I've merged this: https://github.com/apache/arrow/pull/13184
Thanks, -- kou In <20220525.061541.194737838528371525....@clear-code.com> "Re: Merge a pull request with GitHub API" on Wed, 25 May 2022 06:15:41 +0900 (JST), Sutou Kouhei <k...@clear-code.com> wrote: > 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
