+1 on the change, regardless of the discussion around merge button vs script, already starting to "merge" the PR through the script is certainly an improvement!
On Tue, 24 May 2022 at 23:16, 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 >
