Skip to content

Commit

Permalink
feat(scripts/lint-style): more useful line numbers (#12282)
Browse files Browse the repository at this point in the history
This changes slighlty the output of the linter from
```
[...]Mathlib/My/File.lean#L285: ERR_LIN: Line has more than 100 characters
```
to
```
[...]Mathlib/My/File.lean:285 ERR_LIN: Line has more than 100 characters
```

If one then copies the path with the line number and uses that when opening the file in vs code with Ctrl-p, it will set to cursor to the correct line number in question. Also other tools will work with that format, it is also used by pylint, clang etc.




Co-authored-by: Moritz Firsching <firsching@google.com>
  • Loading branch information
2 people authored and Jun2M committed Apr 24, 2024
1 parent bc9ea69 commit 7b35e32
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion scripts/lint-style.py
Original file line number Diff line number Diff line change
Expand Up @@ -359,7 +359,7 @@ def output_message(path, line_nr, code, msg):
msg_type = "warning"
# We are outputting for github. We duplicate path, line_nr and code,
# so that they are also visible in the plaintext output.
print(f"::{msg_type} file={path},line={line_nr},code={code}::{path}#L{line_nr}: {code}: {msg}")
print(f"::{msg_type} file={path},line={line_nr},code={code}::{path}:{line_nr} {code}: {msg}")

def format_errors(errors):
global new_exceptions
Expand Down

0 comments on commit 7b35e32

Please sign in to comment.