master currently failing

Stream: lean4 dev

[Scott Morrison]

master has been failing for the last two days. It seems it is just 5d3ac5f80c852d9b45b354218aee882df3575a7b, the first one with a :cross_mark:. Sorry if I missed a message elsewhere about this.

[Mario Carneiro]

I have an open PR with a quick fix: lean4#2245 . Perhaps someone with merge powers would like to expedite that one? @Leonardo de Moura @Sebastian Ullrich @Gabriel Ebner . It's pretty easy to both confirm the original infinite loop and review the fix

[Mario Carneiro]

Note that the 7 commits there were all added at the same time, so the beginning of the :cross_mark: is not representative. I manually bisected the issue to 83cc0bcc

[Leonardo de Moura]

Merged. Thanks!