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

I am happy to remove some nolints for you!
leanprover-community · Sep 24, 2022 · 5947fb6 · 5947fb6
1 parent 44eb23a
commit 5947fb6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
@@ -40,7 +40,7 @@ src/tactic/interactive.lean : line 10 : ERR_MOD : Module docstring missing, or t
 src/tactic/local_cache.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/monotonicity/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/monotonicity/interactive.lean : line 11 : ERR_MOD : Module docstring missing, or too late
-src/tactic/monotonicity/lemmas.lean : line 12 : ERR_MOD : Module docstring missing, or too late
+src/tactic/monotonicity/lemmas.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/tactic/noncomm_ring.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/nth_rewrite/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/nth_rewrite/congr.lean : line 9 : ERR_MOD : Module docstring missing, or too late