kou opened a new pull request, #13184: URL: https://github.com/apache/arrow/pull/13184
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. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
