Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5143)
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
leanprover-community-bot committed Nov 29, 2020
1 parent fe7b407 commit 5866812
Showing 1 changed file with 24 additions and 25 deletions.
49 changes: 24 additions & 25 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -61,8 +61,6 @@ src/algebra/category/Mon/limits.lean : line 155 : ERR_LIN : Line has more than 1
src/algebra/category/Mon/limits.lean : line 163 : ERR_LIN : Line has more than 100 characters
src/algebra/category/Mon/limits.lean : line 175 : ERR_LIN : Line has more than 100 characters
src/algebra/category/Mon/limits.lean : line 183 : ERR_LIN : Line has more than 100 characters
src/algebra/char_p.lean : line 28 : ERR_LIN : Line has more than 100 characters
src/algebra/char_p.lean : line 71 : ERR_LIN : Line has more than 100 characters
src/algebra/char_zero.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/algebra/char_zero.lean : line 68 : ERR_LIN : Line has more than 100 characters
src/algebra/continued_fractions/computation/approximations.lean : line 21 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -218,6 +216,7 @@ src/analysis/normed_space/bounded_linear_maps.lean : line 153 : ERR_LIN : Line h
src/analysis/normed_space/bounded_linear_maps.lean : line 164 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/bounded_linear_maps.lean : line 260 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/bounded_linear_maps.lean : line 391 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/bounded_linear_maps.lean : line 446 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/finite_dimension.lean : line 171 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/finite_dimension.lean : line 262 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1048 : ERR_LIN : Line has more than 100 characters
Expand All @@ -242,9 +241,9 @@ src/analysis/normed_space/multilinear.lean : line 723 : ERR_LIN : Line has more
src/analysis/normed_space/multilinear.lean : line 761 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 894 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 927 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 221 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 234 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 34 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 628 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 641 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 87 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/arsinh.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/analysis/special_functions/pow.lean : line 1338 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -474,14 +473,14 @@ src/category_theory/limits/shapes/finite_limits.lean : line 186 : ERR_LIN : Line
src/category_theory/limits/shapes/finite_limits.lean : line 193 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/finite_products.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/shapes/finite_products.lean : line 58 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 174 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 194 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 642 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 644 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 647 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 652 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 87 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 90 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 175 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 195 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 659 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 661 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 664 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 669 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 88 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/images.lean : line 91 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/kernel_pair.lean : line 100 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/kernel_pair.lean : line 116 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/kernel_pair.lean : line 17 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -680,11 +679,11 @@ src/data/complex/exponential.lean : line 165 : ERR_LIN : Line has more than 100
src/data/complex/exponential.lean : line 548 : ERR_LIN : Line has more than 100 characters
src/data/complex/exponential.lean : line 841 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 44 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 611 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 616 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 628 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 630 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 652 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 621 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 633 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 635 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 657 : ERR_LIN : Line has more than 100 characters
src/data/dlist/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/dlist/instances.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/data/equiv/denumerable.lean : line 14 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -1122,16 +1121,16 @@ src/group_theory/perm/sign.lean : line 11 : ERR_MOD : Module docstring missing,
src/group_theory/perm/sign.lean : line 111 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 141 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 25 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 261 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 294 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 476 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 617 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 651 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 658 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 661 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 664 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 665 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 266 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 299 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 481 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 622 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 656 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 663 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 666 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 669 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 670 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 671 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 98 : ERR_LIN : Line has more than 100 characters
src/group_theory/presented_group.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/group_theory/presented_group.lean : line 51 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 5866812

Please sign in to comment.