chore(scripts): update nolints.txt (#7867)

I am happy to remove some nolints for you!
leanprover-community · Jun 10, 2021 · 05b7b0b · 05b7b0b
1 parent 4da899c
commit 05b7b0b
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
@@ -112,7 +112,6 @@ src/logic/relation.lean : line 10 : ERR_MOD : Module docstring missing, or too l
 src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/measure_theory/decomposition.lean : line 14 : ERR_MOD : Module docstring missing, or too late
 src/meta/coinductive_predicates.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/order/bounded_lattice.lean : line 15 : ERR_MOD : Module docstring missing, or too late
 src/order/complete_boolean_algebra.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/order/filter/partial.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/order/rel_iso.lean : line 10 : ERR_MOD : Module docstring missing, or too late