lake: command not found

Stream: mathlib4

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/actions/runs/19547578771/job/55970290137?pr=30995
This is failing with the error "lake: command not found"
@Edison Xie says that his repository is also suffering from the same issue so this doesn't seem like a localised problem

[Etienne Marion]

Got the same on #31353

[Etienne Marion]

Merging master seems to have solved it for me.

[Bryan Gin-ge Chen]

My guess is this github incident (now resolved, hopefully): #rss > GitHub Status - Incident History @ 💬

[Chris Henson]

I also saw a failure in CI for getting the Mathlib cache around that time, I'd guess related to the incident as well.