Unmerged commits

Stream: mathlib4

[Antoine Chambert-Loir]

I just observed that my recent PRs that were merged into mathlib are closed with the mention that there were “unmerged commits”. Does this mean that I did something wrong or is it a normal error message?

[Aaron Liu]

This is normal, bors merging your stuff will leave it unmerged

[Weiyi Wang]

Unfortunately this leaves your github profile full of red closed PRs :sweat_smile:

[Kevin Buzzard]

This has been the case for many years