upper/lower case letters in imported file name

Stream: general

[Asei Inoue]

in vscode import Mathlib.Tactic.Linter.MultiGoal does not causes an error.

but in CI import Mathlib.Tactic.Linter.MultiGoal raise an error. (correct file name is Multigoal)

[Asei Inoue]

Shouldn't VSCode also make an error if the case is wrong?

[Mauricio Collares]

This was once fixed in lean4#4538 but then reverted due to performance issues. The reason for the discrepancy is that Mac/Windows have case-insensitive file systems, while Linux doesn't.