Some names are being dropped by subsequent merge commits #320

Closed
cesium12 opened this Issue Dec 14, 2016 · 15 comments

Projects

None yet

6 participants

@cesium12
Contributor

For example, I added my name in dc797a3 but it was immediately removed in b6d31e0. (I'm assuming this was not intentional.)

I can't make heads or tails of the commit history because of all the merges, so I initially had some hope that the file was eventually consistent, but this does not appear to be the case.

@emhoracek
Contributor

I'm checking the diffs before merging... is there any way diffs could be "lying"?

@stuartpb
Contributor

If you're doing it via GitHub's merge UI, yeah, probably.

FWIW, my name appears to have been cut in that merge as well.

@cesium12
Contributor

Is it possible that the multiple maintainers trying to merge pull requests concurrently are writing over each other?

@hurtstotouchfire
Contributor

Is it possible that #228 would fix this?

@stuartpb
Contributor

It's possible (though it wouldn't fix it retroactively, of course). I'm not privy to the inner workings of GitHub's featureset.

More likely, though, is that it's a matter of commits being authored based on the tip of master at the time the merge page was loaded, meaning that the conflicts in question won't be observed, period.

@hurtstotouchfire
Contributor

My suspicion is that this is just user error. I've never had this problem with the github merge ui before. Not invisibly anyway.

@stuartpb
Contributor

Yeah, I think #320 (comment) is probably accurate - one maintainer opens a PR merge based on the current master, another maintainer opens another merge based on the same master, and the content of the second merge overrides the first one.

@stuartpb
Contributor

In other words, I think it's a GitHub bug, based on their merge functionality not having been written to handle a potential race between two separate merges.

@stuartpb
Contributor
stuartpb commented Dec 14, 2016 edited

I've contacted GitHub Support about this.

@mezz
Contributor
mezz commented Dec 14, 2016

This happened the first time I tried to commit. It took me a little while to edit the page from the Github interface, and by the time I went to merge it was 1 added line and 2 (recent) lines removed.

I abandoned that commit and made a new one more quickly and had no issue.

@hurtstotouchfire
Contributor

Yeah I think the github UI is causing issues. Some of these deletions were introduced by resolving conflicts in the web UI.

@stuartpb
Contributor

#376 didn't fix this; there are still a lot of names missing from the list (mine, for one).

@cesium12
Contributor

As well as mine. :P

@danielquinn

@stuartpb and @cesium12 now that the project has changed to using individual files rather than editing a single document, this problem should go away. I suppose you could just re-add your names now using the new system.

@stuartpb
Contributor

It would also be fixed the old way, as GitHub fixed the underlying bug after I pinged support about it:

On 12/14/2016 6:54 PM, Scott J. Goldman wrote:

Hey Stuart -

Sorry for the trouble. Turns out there was a bug in the conflict resolver where in certain cases, the commit created might delete some lines created in base repository if they raced between you opening the conflict editor and submitting the resolution. You can see the merge commit (generated by the conflict resolver) in #266 deletes the lines, which got merged into master.

We've fixed the bug so it shouldn't happen again, and I did want to apologize. It was definitely a crummy bug.

Thanks for pointing it out!
-sjg

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment