GitHub merge-conflict label

Stream: general

[Martin Dvořák]

When I get a merge-conflict label on a Mathlib PR, can I view on GitHub where the conflict is?

[Johan Commelin]

Usually there is a button "Resolve conflicts" close to where the merge button normally is.

[Martin Dvořák]

Ah! It's just a conflict in the Mathlib.lean file. IMO it's pretty dumb we have to maintain this file.

[Johan Commelin]

Yep. At least we should have a bot that fixes these conflicts.

[Martin Dvořák]

The current merge-conflict mechanisms imply that other PRs can kick my PR out / to the end of #queue .

[Jireh Loreaux]

I think several maintainers look at the queue in both ascending and descending order. I do anyway.