[Development] GitHub Pull requests
mwoehlke.floss at gmail.com
Thu Mar 12 16:17:57 CET 2020
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...
>>> 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.
More information about the Development