Properly merging pull requests

[Lawrence Velázquez]

> On Nov 3, 2016, at 12:19 PM, Sterling Smith <smithsp at fusion.gat.com> wrote:
> 
> The user will not learn if you change it under his/her feet.  I think
> that you should make line by comments of changes that need to be made
> in the files tab of the pull request and ask the pull request
> submitter to make those changes.

While this is all fine in the abstract, in practice committers have
always felt free to improve contributors' patches before committing,
especially if said improvements are minor.

> Or you can make them yourself and push them to the branch of the pull
> request and ask the submitter if s/he is OK with them.

The contributor must first allow us to modify their PR branch:

https://help.github.com/articles/allowing-changes-to-a-pull-request-branch-created-from-a-fork

This seems very useful. Perhaps we should request that all contributors
do this when opening PRs.

vq