You are viewing a plain text version of this content. The canonical link for it is here.
Posted to issues@arrow.apache.org by "Kouhei Sutou (Jira)" <ji...@apache.org> on 2022/05/18 03:38:00 UTC

[jira] [Created] (ARROW-16602) [Dev] Use GitHub API to merge pull request

Kouhei Sutou created ARROW-16602:
------------------------------------

             Summary: [Dev] Use GitHub API to merge pull request
                 Key: ARROW-16602
                 URL: https://issues.apache.org/jira/browse/ARROW-16602
             Project: Apache Arrow
          Issue Type: Improvement
          Components: Developer Tools
            Reporter: Kouhei Sutou
            Assignee: Kouhei Sutou


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 message was sent by Atlassian Jira
(v8.20.7#820007)