Skip to content

Commit

Permalink
Make the semicolon check not complain about itself.
Browse files Browse the repository at this point in the history
Remove now-fixed copyright exceptions.
  • Loading branch information
grunweg committed May 27, 2024
1 parent 12960f7 commit 38b96fc
Showing 1 changed file with 3 additions and 6 deletions.
9 changes: 3 additions & 6 deletions scripts/style-exceptions-new.txt
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
-- Style exceptions specific to the "new" linter in Lean: until the old linter is still around, we keep these in a separate file.
-- If possible, put style exceptions into `style-exceptions.txt`.
-- This is also why this file is not updated automatically.

-- Three cases of a commented #align; that's fine, I guess.
Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean : line 133 : ERR_LIN : Line has 113 characters, which is more than 100
Expand All @@ -17,9 +18,5 @@ Archive/Sensitivity.lean : line 2 : ERR_COP : Malformed or missing copyright hea
Archive/Sensitivity.lean : line 3 : ERR_COP : Malformed or missing copyright header: Second line should be "Released under Apache 2.0 license as described in the file LICENSE."
Archive/Sensitivity.lean : line 4 : ERR_COP : Malformed or missing copyright header: The third line should describe the file's main authors

-- TODO: these files are missing copyright *years*
Mathlib/Algebra/Polynomial/PartialFractions.lean : line 2 : ERR_COP : Malformed or missing copyright header: Copyright line is malformed
Mathlib/Analysis/Complex/Basic.lean : line 2 : ERR_COP : Malformed or missing copyright header: Copyright line is malformed
Mathlib/Analysis/Complex/OperatorNorm.lean : line 2 : ERR_COP : Malformed or missing copyright header: Copyright line is malformed
Mathlib/Analysis/Complex/RealDeriv.lean : line 2 : ERR_COP : Malformed or missing copyright header: Copyright line is malformed
Mathlib/CategoryTheory/Limits/Shapes/Equivalence.lean : line 2 : ERR_COP : Malformed or missing copyright header: Copyright line is malformed
-- The "grep for ;" check finds itself.
Mathlib/Tactic/Linter/TextBased.lean : line 301 : ERR_SEM : Line contains a space before a semicolon

0 comments on commit 38b96fc

Please sign in to comment.