mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard
verified publisher icon leanprover-community

chore: remove style linter for windows line endings

Open grunweg opened this issue 1 year ago • 2 comments

Now that the Lean frontend normalises all line endings to LF (since leanprover/lean4#3903), this check is not necessary any more. It is also one fewer Python linter to rewrite in Lean.

Open in Gitpod

grunweg avatar May 21 '24 20:05 grunweg

I think that we should still mandate LF line endings to avoid PRs that have large diffs because of change between two line endings.

urkud avatar May 22 '24 05:05 urkud

Good point - let me rewrite this one in Lean instead. awaiting-author

grunweg avatar May 22 '24 12:05 grunweg

In #13199, I have rewritten this linter: let me close this PR.

grunweg avatar May 25 '24 15:05 grunweg