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

I am happy to remove some nolints for you!
leanprover-community · Dec 26, 2020 · 768497c · 768497c
1 parent 666035f
commit 768497c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/scripts/copy-mod-doc-exceptions.txt b/scripts/copy-mod-doc-exceptions.txt
@@ -86,7 +86,7 @@ src/algebra/group/with_one.lean : line 9 : ERR_MOD : Module docstring missing, o
 src/algebra/group_action_hom.lean : line 270 : ERR_LIN : Line has more than 100 characters
 src/algebra/group_power/basic.lean : line 414 : ERR_LIN : Line has more than 100 characters
 src/algebra/group_power/basic.lean : line 501 : ERR_LIN : Line has more than 100 characters
-src/algebra/group_power/lemmas.lean : line 536 : ERR_LIN : Line has more than 100 characters
+src/algebra/group_power/lemmas.lean : line 582 : ERR_LIN : Line has more than 100 characters
 src/algebra/group_with_zero/power.lean : line 153 : ERR_LIN : Line has more than 100 characters
 src/algebra/invertible.lean : line 216 : ERR_LIN : Line has more than 100 characters
 src/algebra/invertible.lean : line 224 : ERR_LIN : Line has more than 100 characters