On 10/18/2016 08:03 PM, Benda Xu wrote:
> This will be an important reference. Please consider adding it into the
> wiki after we reach a wider consensus on how to merge pull request on
> github.

It's been there for a long time:


(that's the way I prefer to merge pull requests, too).

Reply via email to