[Merged by Bors] - lint(scripts/lint-style): Add linting for lower-case clashes #6825
Conversation
|
The linter output looks a bit strange in the test branch on github actions, the input and output lines seem to get interspersed. |
leanprover-community-mathlib4-bot
added
ready-to-merge
|
I noticed that and I wonder if it is due to the options set at the beginning of the file. On my computer, the output is what I expect it to be. I can remove all printouts other that the clashing filenames, if it is preferable. |
Introduce a global check on git-managed filenames in the whole repository, making sure that the filenames are distinct also up to upper/lower casing. Fixes an issue that came up when two file names that only differed by their casing were imported in a case-insensitive operating system. As a check, I pushed [branch#adomani/testUpperLowerLinter](https://github.com/leanprover-community/mathlib4/tree/adomani/testUpperLowerLinter) from this PR containing `CODe_OF_CONDUCT.md` alongside `CODE_OF_CONDUCT.md`. The [linter failed](https://github.com/leanprover-community/mathlib4/actions/runs/5997399826/job/16263715177) on that branch.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
Introduce a global check on git-managed filenames in the whole repository, making sure that the filenames are distinct also up to upper/lower casing.
Fixes an issue that came up when two file names that only differed by their casing were imported in a case-insensitive operating system.
As a check, I pushed branch#adomani/testUpperLowerLinter from this PR containing
CODe_OF_CONDUCT.mdalongsideCODE_OF_CONDUCT.md. The linter failed on that branch.