mk_all reports done, but not on CI

Stream: mathlib4

[Alex Meiburg]

CI is reporting

Please run 'lake exe mk_all' to regenerate the import all files
Error: Process completed with exit code 1.

but when I run that command locally, it tells me

% lake exe mk_all
No update necessary

and makes no changes. My local repo is up to the date with what I've pushed.

[Aaron Liu]

The problem is the error above

[Aaron Liu]

specifically, in the section "build pr-branch tools (test)"

[Alex Meiburg]

Ah, right you are. I guess the fact that I touched docs/1000.yaml made it decide to re-build the tools. Funny, but ok. But it's failing to build the tools.

[Bryan Gin-ge Chen]

This is probably the same issue as in #mathlib4 > CI errors in "build pr-branch tools" step