Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5158)
Browse files Browse the repository at this point in the history
I am happy to remove some nolints for you!
  • Loading branch information
leanprover-community-bot committed Dec 1, 2020
1 parent c3f4d1b commit b846aa5
Showing 1 changed file with 8 additions and 10 deletions.
18 changes: 8 additions & 10 deletions scripts/copy-mod-doc-exceptions.txt
Expand Up @@ -1154,8 +1154,8 @@ src/linear_algebra/basis.lean : line 93 : ERR_LIN : Line has more than 100 chara
src/linear_algebra/char_poly/coeff.lean : line 190 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/char_poly/coeff.lean : line 24 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/char_poly/coeff.lean : line 26 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/determinant.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/linear_algebra/determinant.lean : line 257 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/determinant.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/linear_algebra/determinant.lean : line 258 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/direct_sum/finsupp.lean : line 24 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/direct_sum/tensor_product.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/linear_algebra/dual.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -1389,13 +1389,11 @@ src/ring_theory/ideal/operations.lean : line 865 : ERR_LIN : Line has more than
src/ring_theory/ideal/operations.lean : line 93 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 95 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 991 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 116 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 121 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 197 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 412 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 413 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 414 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 505 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 118 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 123 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 199 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 444 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_closure.lean : line 535 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_domain.lean : line 104 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_domain.lean : line 124 : ERR_LIN : Line has more than 100 characters
src/ring_theory/integral_domain.lean : line 129 : ERR_LIN : Line has more than 100 characters
Expand All @@ -1415,7 +1413,7 @@ src/ring_theory/jacobson_ideal.lean : line 87 : ERR_LIN : Line has more than 100
src/ring_theory/jacobson_ideal.lean : line 97 : ERR_LIN : Line has more than 100 characters
src/ring_theory/localization.lean : line 1188 : ERR_LIN : Line has more than 100 characters
src/ring_theory/localization.lean : line 1350 : ERR_LIN : Line has more than 100 characters
src/ring_theory/localization.lean : line 1528 : ERR_LIN : Line has more than 100 characters
src/ring_theory/localization.lean : line 1529 : ERR_LIN : Line has more than 100 characters
src/ring_theory/localization.lean : line 870 : ERR_LIN : Line has more than 100 characters
src/ring_theory/multiplicity.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/ring_theory/multiplicity.lean : line 142 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit b846aa5

Please sign in to comment.