mathlib4#838

Stream: mathlib4

[Ruben Van de Velde]

Scott told bors to merge this, but it doesn't seem to be doing anything - could someone take a look?

[Kevin Buzzard]

Scott mentioned in an earlier thread that Bors had crashed, any posted a link which probably only works for maintainers (or, at least, didn't work for me)

[Bryan Gin-ge Chen]

Yeah, something strange seems to be going on. I've filed a report at the bors repo: https://github.com/bors-ng/bors-ng/issues/1578