[Development] GitHub Pull requests

[Edward Welbourne]

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 ?

	Eddy.