CI: duplicate check for case collisions

Stream: mathlib4

[Michael Rothgang]

The "style lint" step of the build workflow currently checks twice if there are different files whose lower-case name is different: once by calling in the case checker action action, and again in lint-style.sh(just for the .lean files). Is there a reason for this duplication? Can one of them be removed?

For just the .lean files, the check is easy to rewrite in Lean (which would remove a dependency on an external action, which I consider a small plus in principle): that said, if checking the entire repo is useful, I also understand.

[Johan Commelin]

I guess some os's get into trouble if such a clash occurs?

[Johan Commelin]

So let's check the whole repo and dedup the linting

[Michael Rothgang]

Johan Commelin said:

I guess some os's get into trouble if such a clash occurs?

Windows, I believe

[Michael Rothgang]

(Though just for building mathlib, perhaps that's not an issue...)

[Michael Rothgang]

#15027