The case for small diffs in Pull Requests

[qznc via Digitalmars-d]

On Thursday, 21 July 2016 at 06:04:24 UTC, default0 wrote:
> On Thursday, 21 July 2016 at 03:30:34 UTC, Walter Bright wrote:
>> I've looked at many PRs that consisted of multiple commits.
>>
>> The trouble with them is:
>>
>> 1. they often have nothing in particular to do with each other
>>
>> 2. I may want to pull a subset of the commits, but the only 
>> option I have is all or nothing
>
> As far as I'm aware git offers the option of cherry picking 
> commits. It will not mark the PR as merged or generally not be 
> what you are looking for, but maybe it's a usable workaround :)

Git does, but Github does not.

D uses a bot [0] to do the merging. Afaik the process is that an 
authorized person (Walter, Andrei, etc) comment with "Auto-merge 
toggled on", then the bot toggles the merge after it ensures that 
tests pass.

In theory, the bot could be extended to merge only certain 
commits and exclude others. That might solve (2), but it muddles 
the review process.

(1) is not to be solved. If commits have nothing to do with each 
other then the should be in separate pull requests.

[0] https://github.com/braddr/d-tester