Skip to content

Commit

Permalink
Update for #11913.
Browse files Browse the repository at this point in the history
  • Loading branch information
@grunweg
grunweg committed Apr 21, 2024
1 parent 3586a9d commit 58875d4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion scripts/style-exceptions.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ Mathlib/Data/UnionFind.lean : line 10 : ERR_MOD : Module docstring missing, or t
Mathlib/FieldTheory/RatFunc.lean : line 1 : ERR_NUM_LIN : 1900 file contains 1781 lines, try to split it up
Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean : line 1 : ERR_NUM_LIN : 1800 file contains 1607 lines, try to split it up
Mathlib/GroupTheory/MonoidLocalization.lean : line 1 : ERR_NUM_LIN : 2300 file contains 2153 lines, try to split it up
Mathlib/GroupTheory/Subgroup/Basic.lean : line 1 : ERR_NUM_LIN : 4000 file contains 3878 lines, try to split it up
Mathlib/GroupTheory/Subgroup/Basic.lean : line 1 : ERR_NUM_LIN : 3800 file contains 3629 lines, try to split it up
Mathlib/GroupTheory/Submonoid/Operations.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1504 lines, try to split it up
Mathlib/Init/Data/Int/Basic.lean : line 12 : ERR_MOD : Module docstring missing, or too late
Mathlib/Init/Data/Nat/Basic.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand Down

0 comments on commit 58875d4

Please sign in to comment.