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

I am happy to remove some nolints for you!
leanprover-community · Aug 22, 2021 · 8a96d00 · 8a96d00
1 parent f915106
commit 8a96d00
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
@@ -73,8 +73,8 @@ src/tactic/converter/interactive.lean : line 53 : ERR_LIN : Line has more than 1
 src/tactic/converter/old_conv.lean : line 272 : ERR_LIN : Line has more than 100 characters
 src/tactic/converter/old_conv.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/tactic/core.lean : line 17 : ERR_MOD : Module docstring missing, or too late
-src/tactic/core.lean : line 2196 : ERR_LIN : Line has more than 100 characters
-src/tactic/core.lean : line 2357 : ERR_LIN : Line has more than 100 characters
+src/tactic/core.lean : line 2194 : ERR_LIN : Line has more than 100 characters
+src/tactic/core.lean : line 2355 : ERR_LIN : Line has more than 100 characters
 src/tactic/delta_instance.lean : line 67 : ERR_LIN : Line has more than 100 characters
 src/tactic/delta_instance.lean : line 75 : ERR_LIN : Line has more than 100 characters
 src/tactic/delta_instance.lean : line 8 : ERR_MOD : Module docstring missing, or too late
@@ -83,9 +83,9 @@ src/tactic/ext.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/tactic/fin_cases.lean : line 121 : ERR_LIN : Line has more than 100 characters
 src/tactic/fin_cases.lean : line 13 : ERR_MOD : Module docstring missing, or too late
 src/tactic/find.lean : line 8 : ERR_MOD : Module docstring missing, or too late
-src/tactic/generalizes.lean : line 118 : ERR_LIN : Line has more than 100 characters
+src/tactic/generalizes.lean : line 117 : ERR_LIN : Line has more than 100 characters
 src/tactic/hint.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-src/tactic/induction.lean : line 1337 : ERR_RNT : Reserved notation outside tactic.reserved_notation
+src/tactic/induction.lean : line 1329 : ERR_RNT : Reserved notation outside tactic.reserved_notation
 src/tactic/interactive.lean : line 1063 : ERR_LIN : Line has more than 100 characters
 src/tactic/interactive.lean : line 385 : ERR_LIN : Line has more than 100 characters
 src/tactic/interactive.lean : line 649 : ERR_LIN : Line has more than 100 characters