Skip to content

Commit

Permalink
Oops
Browse files Browse the repository at this point in the history
  • Loading branch information
grunweg committed May 27, 2024
1 parent 1eab438 commit e09bf3b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Linter/TextBased.lean
Original file line number Diff line number Diff line change
Expand Up @@ -154,7 +154,7 @@ def lint_file (path : System.FilePath) : IO Bool := do
-- XXX: this list is currently not sorted: for github, that's probably fine
let errors := Array.flatten all_output
formatErrors errors
return errors.size == 0
return errors.size > 0

/-- Lint all files referenced in a given import-only file.
Return the number of files which had new style errors. -/
Expand Down

0 comments on commit e09bf3b

Please sign in to comment.