[Development] GitHub Pull requests

[Matthew Woehlke]

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