Hi Lenz, On Tue, Sep 8, 2020 at 12:02 AM Lenz Grimmer <lgrimmer@suse.com> wrote:
Note: src/script/ptl-tool.py is a script tool for merging pull requests that automatically adds "Reviewed-by" to the merge commit message for you. It adds the message for GitHub review approvals or comments indicating "Reviewed-by...".
Nice, good to know. But this requires push privileges into the corresponding branch, correct?
I believe so.
Or is that a give if one has the permissions to merge PRs via the github web interface? I haven't dared trying pushing directly into master yet ;)
By the way, ptl-tool.py seems to use a slightly different format than github when it comes to referring to the pull request:
[SNIP] Author: Patrick Donnelly <pdonnell@redhat.com> Date: Thu Sep 3 10:08:42 2020 -0700
Merge PR #36546 into master
* refs/pull/36546/head: vstart_runner: log commands in a more usable form
Reviewed-by: Patrick Donnelly <pdonnell@redhat.com> Reviewed-by: Ernesto Puerta <epuertat@redhat.com> [SNIP]
pt-tool indicates the destination branch, while github focuses on the source branch. Is there a point in trying to have a more consistent way of referring to the pull request ID and the branches involved?
It was a choice I made early on but not for any particular good reason. I don't really see a point in changing anything as the information about the source branch on Github is not particularly useful. -- Patrick Donnelly, Ph.D. He / Him / His Principal Software Engineer Red Hat Sunnyvale, CA GPG: 19F28A586F808C2402351B93C3301A3E258DD79D