Bors stuck

Stream: mathlib4

[Ruben Van de Velde]

It seems like #11874 passed in bors six hours ago and bors has been stuck ever since. Anyone around who can take a look?

[Bryan Gin-ge Chen]

The bors status page (only viewable by maintainers, I think) thinks that batch is still running: https://mathlib-bors-ca18eefec4cb.herokuapp.com/repositories/16/log

Bors has an 8 hour timeout so if it's still stuck in 2 hours or so then let's ping Mario / Rob who may be able to reset the bors machine.

[Bryan Gin-ge Chen]

I commented on the PR, looks like bors was waiting for a step that got removed from CI, so we just have to remove it from bors.toml. Should be a quick fix.

[Michael Rothgang]

I've pushed that quick fix to the PR.

[Michael Rothgang]

I've also added a commit replacing the last reference to the shell script: that workflow already ran successfully on the PR.

[Bryan Gin-ge Chen]

Thanks! I've put it back on the bors queue.

[Michael Rothgang]

Fingers crossed it works this time!

[Yuyang Zhao]

Bors has been running for 6 hours in #17925.

[Bryan Gin-ge Chen]

Ah, it seems bors crashed again. I'll put it back on the queue.

[Ruben Van de Velde]

Is https://mathlib-bors-ca18eefec4cb.herokuapp.com/repositories/16 supposed to say "Application error"?