Working with Git

[Ryan Schmidt]

On Oct 6, 2016, at 06:09, Chris Jones <jonesc at hep.phy.cam.ac.uk> wrote:
> 
> 
> 
>> On 06/10/16 11:43, Mojca Miklavec wrote:
>> 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.
> 
> I guess one option would be to reject the request, providing information on why, and leave it to the user to fix the issues and resubmit a new request. If they need to they can rebase/revert their local checkout back to before their changes, to remove the bad commits from the history.

I assumed that in such a case, where the contributor is (or we are) making several commits to fix mistakes in a submission, we would use a "squash merge" (?) to combine all the changes in the pull request into a single commit on master. The GitHub web interface provides an option for this. If we want to rebase instead of merge (?) we would need to write up a procedure for how that's accomplished.