Lost `end` in merge

Stream: general

[Stuart Presnell]

I resolved a merge conflict using the GitHub web interface, but the end at the end of one of the lemmas in my PR was unified with the end at the end of a lemma that was being merged, and so one of the two ends was lost. This is a trivial issue, but I failed to spot it this time and it caused the PR to fail CI. Is there any way to tweak things so that this unwanted unification doesn't happen, or do I just need to be a little more attentive in future?

[Stuart Presnell]

(Or, perhaps, would I do better to resolve merge conflicts without going through the web interface?)

[Eric Wieser]

Local merge tools can often have better heuristics than the one included with git (that I assume GitHub uses).

[Eric Wieser]

Note also that our CI tends to pick the slower cache (close to your branch but far from master) when faced with a choice; you can often rebuild faster locally by running leanproject get-cache --fallback=download-first after merging, which gets a different cache to what CI uses (far from your branch but close to master)