+1 -----Original Message----- From: Sutou Kouhei <k...@clear-code.com> Sent: Wednesday, May 18, 2022 11:43 AM To: dev@arrow.apache.org Subject: Merge a pull request with GitHub API
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 IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.
