Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#4910)
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 5, 2020
1 parent 189063b commit 834d491
Showing 1 changed file with 13 additions and 13 deletions.
26 changes: 13 additions & 13 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -190,16 +190,16 @@ src/analysis/calculus/mean_value.lean : line 491 : ERR_LIN : Line has more than
src/analysis/calculus/mean_value.lean : line 682 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/mean_value.lean : line 910 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/tangent_cone.lean : line 251 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 1444 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 1855 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 2460 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 2478 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 1456 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 1867 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 2489 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 2507 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 400 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 412 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 428 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 583 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 735 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 892 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 579 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 743 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 900 : ERR_LIN : Line has more than 100 characters
src/analysis/complex/basic.lean : line 187 : ERR_LIN : Line has more than 100 characters
src/analysis/complex/polynomial.lean : line 60 : ERR_LIN : Line has more than 100 characters
src/analysis/convex/basic.lean : line 1131 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -321,7 +321,7 @@ src/category_theory/adjunction/limits.lean : line 42 : ERR_LIN : Line has more t
src/category_theory/adjunction/limits.lean : line 50 : ERR_LIN : Line has more than 100 characters
src/category_theory/adjunction/limits.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/category/Kleisli.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/category_theory/closed/cartesian.lean : line 326 : ERR_LIN : Line has more than 100 characters
src/category_theory/closed/cartesian.lean : line 329 : ERR_LIN : Line has more than 100 characters
src/category_theory/comma.lean : line 47 : ERR_LIN : Line has more than 100 characters
src/category_theory/concrete_category/basic.lean : line 112 : ERR_LIN : Line has more than 100 characters
src/category_theory/concrete_category/basic.lean : line 116 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1021,8 +1021,8 @@ src/field_theory/chevalley_warning.lean : line 80 : ERR_LIN : Line has more than
src/field_theory/finite/basic.lean : line 53 : ERR_LIN : Line has more than 100 characters
src/field_theory/fixed.lean : line 27 : ERR_LIN : Line has more than 100 characters
src/field_theory/fixed.lean : line 77 : ERR_LIN : Line has more than 100 characters
src/field_theory/intermediate_field.lean : line 150 : ERR_LIN : Line has more than 100 characters
src/field_theory/intermediate_field.lean : line 155 : ERR_LIN : Line has more than 100 characters
src/field_theory/intermediate_field.lean : line 160 : ERR_LIN : Line has more than 100 characters
src/field_theory/minimal_polynomial.lean : line 116 : ERR_LIN : Line has more than 100 characters
src/field_theory/mv_polynomial.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/field_theory/primitive_element.lean : line 29 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1214,7 +1214,7 @@ src/linear_algebra/multilinear.lean : line 78 : ERR_LIN : Line has more than 100
src/linear_algebra/special_linear_group.lean : line 53 : ERR_LIN : Line has more than 100 characters
src/logic/basic.lean : line 491 : ERR_LIN : Line has more than 100 characters
src/logic/basic.lean : line 568 : ERR_LIN : Line has more than 100 characters
src/logic/basic.lean : line 836 : ERR_LIN : Line has more than 100 characters
src/logic/basic.lean : line 864 : ERR_LIN : Line has more than 100 characters
src/logic/function/basic.lean : line 312 : ERR_LIN : Line has more than 100 characters
src/logic/function/basic.lean : line 478 : ERR_LIN : Line has more than 100 characters
src/logic/function/basic.lean : line 518 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1383,9 +1383,9 @@ src/order/zorn.lean : line 241 : ERR_LIN : Line has more than 100 characters
src/order/zorn.lean : line 47 : ERR_LIN : Line has more than 100 characters
src/ring_theory/adjoin_root.lean : line 129 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 225 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 238 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 274 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 418 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 240 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 289 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 433 : ERR_LIN : Line has more than 100 characters
src/ring_theory/dedekind_domain.lean : line 112 : ERR_LIN : Line has more than 100 characters
src/ring_theory/dedekind_domain.lean : line 21 : ERR_LIN : Line has more than 100 characters
src/ring_theory/dedekind_domain.lean : line 23 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 834d491

Please sign in to comment.