Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5554)
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 Jan 1, 2021
1 parent 54bf708 commit d2bde11
Showing 1 changed file with 23 additions and 28 deletions.
51 changes: 23 additions & 28 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -135,18 +135,15 @@ src/algebraic_geometry/sheafed_space.lean : line 50 : ERR_LIN : Line has more th
src/algebraic_geometry/sheafed_space.lean : line 82 : ERR_LIN : Line has more than 100 characters
src/algebraic_geometry/stalks.lean : line 47 : ERR_LIN : Line has more than 100 characters
src/algebraic_geometry/stalks.lean : line 48 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 206 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 349 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 574 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 683 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 763 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 654 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 734 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 161 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 204 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 242 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 900 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 901 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 904 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 944 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 849 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 850 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 853 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 893 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/deriv.lean : line 1104 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/deriv.lean : line 326 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/fderiv.lean : line 1928 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -200,20 +197,20 @@ src/analysis/normed_space/bounded_linear_maps.lean : line 392 : ERR_LIN : Line h
src/analysis/normed_space/bounded_linear_maps.lean : line 447 : 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 1061 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1098 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1295 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1063 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1100 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1297 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1305 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1329 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1335 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1336 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1402 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1547 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1556 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 348 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 814 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 833 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1299 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1307 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1331 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1337 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1338 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1404 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1549 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1558 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 350 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 816 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 835 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 1022 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 110 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 143 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -940,9 +937,9 @@ src/deprecated/subring.lean : line 133 : ERR_LIN : Line has more than 100 charac
src/deprecated/subring.lean : line 15 : ERR_LIN : Line has more than 100 characters
src/deprecated/subring.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/dynamics/circle/rotation_number/translation_number.lean : line 264 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 239 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 110 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 258 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 66 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 91 : ERR_LIN : Line has more than 100 characters
src/field_theory/chevalley_warning.lean : line 144 : ERR_LIN : Line has more than 100 characters
src/field_theory/chevalley_warning.lean : line 80 : ERR_LIN : Line has more than 100 characters
src/field_theory/finite/basic.lean : line 21 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1285,10 +1282,8 @@ src/order/zorn.lean : line 121 : ERR_LIN : Line has more than 100 characters
src/order/zorn.lean : line 235 : ERR_LIN : Line has more than 100 characters
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/algebra_tower.lean : line 213 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 228 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 277 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 421 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 103 : ERR_LIN : Line has more than 100 characters
src/ring_theory/algebra_tower.lean : line 219 : 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 d2bde11

Please sign in to comment.