Skip to content

Commit

Permalink
chore: remove style linter for windows line endings
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
grunweg committed May 21, 2024
1 parent 27b3df7 commit 2931c6b
Showing 1 changed file with 0 additions and 6 deletions.
6 changes: 0 additions & 6 deletions scripts/lint-style.py
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,6 @@
ERR_IBY = 11 # isolated by
ERR_DOT = 12 # isolated or low focusing dot
ERR_SEM = 13 # the substring " ;"
ERR_WIN = 14 # Windows line endings "\r\n"
ERR_TWS = 15 # trailing whitespace
ERR_CLN = 16 # line starts with a colon
ERR_IND = 17 # second line not correctly indented
Expand Down Expand Up @@ -160,9 +159,6 @@ def line_endings_check(lines, path):
errors = []
newlines = []
for line_nr, line in lines:
if "\r\n" in line:
errors += [(ERR_WIN, line_nr, path)]
line = line.replace("\r\n", "\n")
if line.endswith(" \n"):
errors += [(ERR_TWS, line_nr, path)]
line = line.rstrip() + "\n"
Expand Down Expand Up @@ -385,8 +381,6 @@ def format_errors(errors):
output_message(path, line_nr, "ERR_DOT", "Line is an isolated focusing dot or uses . instead of ·")
if errno == ERR_SEM:
output_message(path, line_nr, "ERR_SEM", "Line contains a space before a semicolon")
if errno == ERR_WIN:
output_message(path, line_nr, "ERR_WIN", "Windows line endings (\\r\\n) detected")
if errno == ERR_TWS:
output_message(path, line_nr, "ERR_TWS", "Trailing whitespace detected on line")
if errno == ERR_CLN:
Expand Down

0 comments on commit 2931c6b

Please sign in to comment.