diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt index c67d6bddc8a86..d155af65073e5 100644 --- a/scripts/style-exceptions.txt +++ b/scripts/style-exceptions.txt @@ -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