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

I am happy to remove some nolints for you!
leanprover-community · Mar 9, 2022 · 1f6a2e9 · 1f6a2e9
1 parent 2a3ecad
commit 1f6a2e9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
@@ -45,7 +45,7 @@ src/tactic/ext.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/find.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/hint.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/interactive.lean : line 10 : ERR_MOD : Module docstring missing, or too late
-src/tactic/lint/default.lean : line 11 : ERR_MOD : Module docstring missing, or too late
+src/tactic/lint/default.lean : line 12 : ERR_MOD : Module docstring missing, or too late
 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