Recent regression: `test` step fails in CI, not locally

Stream: mathlib4

[Michael Rothgang]

#17555 has a curious error: the test step of CI fails, but running lake test locally passes (as does running the test file in VS Code). This happened since a recent rebase on master - could this be a recent regression?

[Damiano Testa]

Could it be that it is consequence of uploading the cache of the test files? I'm not sure why, but I've seen some weird behaviour between cache and linter warnings in the past. :shrug:

[Bryan Gin-ge Chen]

(I can't make heads or tails of the error message myself, but here's a link to the failure in question for reference.)

[Damiano Testa]

This test is using the old trick to set and unset the linter option. That may no longer be needed and may affect the tests?

[Damiano Testa]

I don't really understand what happened, but pulling to my computer locally created some git confusion. I fixed the confusion, update the linter message that appeared to be missing two single quotes, and now the tests passed.