On 12/03/2020 01.55, Thiago Macieira wrote: > On Wednesday, 11 March 2020 03:48:24 PDT Edward Welbourne wrote: >> Matthew Woehlke (10 March 2020 20:24) wrote: >>> In an ideal world... >> >> [snip] >> >>> Note that I believe nothing needs to be done to "merge" the GitHub PR; >>> if the commits become reachable from the target branch, it should >>> automatically get marked as "merged". >> >> Given that gerrit cherry-picks the change submitted onto the branch it's >> sent to, the commit the user originally pushed doesn't become reachable. >> Will GitHub recognise the cherry-pick as resolving the PR ? > > I doubt it. It doesn't recognise when I do that manually. It only recognises > when GitHub itself dos the rebase prior to application. All other cases, the > PR needs to be closed as if it got rejected.
Actually, if the PR has 'code owners may modify this' permission, the bot *might* be able to force-push the branch after rebasing, which would cause it to show up as 'merged' rather than 'closed'. But, yeah, probably this will (alas) require a little more effort from the bot. -- Matthew _______________________________________________ Development mailing list [email protected] https://lists.qt-project.org/listinfo/development
