Working with Git

[Mojca Miklavec]

On 6 October 2016 at 09:39, Chris Jones wrote:
>> How do I take the user's pull request, make additional changes, and commit
>> them to our master?
>
> Anyone can commit to the branch created by the user for the pull request. So
> you can just checkout that branch yourself, make changes, commit and push
> them back to the branch, and thus the merge request.

Interesting, thank you, I didn't know (or think of) that.

My next question was going to be: what happens when user submits a
pull request that needs quite a bit of editing? Say that the user
first changes all the whitespacing together with content changes and
potentially does some other mistakes like increasing epoch for no good
reason etc. Of course he can then make another commit that changes
that back, but we would end up with super weird history for no good
reason unless we take the liberty to modify the commits (heavily)
before accepting them.

Mojca