Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5459)
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 Dec 21, 2020
1 parent d79105e commit ca2e536
Showing 1 changed file with 18 additions and 18 deletions.
36 changes: 18 additions & 18 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -76,7 +76,7 @@ src/algebra/continued_fractions/computation/translations.lean : line 17 : ERR_LI
src/algebra/continued_fractions/computation/translations.lean : line 22 : ERR_LIN : Line has more than 100 characters
src/algebra/continued_fractions/computation/translations.lean : line 34 : ERR_LIN : Line has more than 100 characters
src/algebra/continued_fractions/computation/translations.lean : line 92 : ERR_LIN : Line has more than 100 characters
src/algebra/continued_fractions/convergents_equiv.lean : line 281 : ERR_LIN : Line has more than 100 characters
src/algebra/continued_fractions/convergents_equiv.lean : line 283 : ERR_LIN : Line has more than 100 characters
src/algebra/continued_fractions/terminated_stable.lean : line 28 : ERR_LIN : Line has more than 100 characters
src/algebra/direct_limit.lean : line 242 : ERR_LIN : Line has more than 100 characters
src/algebra/direct_limit.lean : line 464 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -976,16 +976,16 @@ src/field_theory/minimal_polynomial.lean : line 250 : ERR_LIN : Line has more th
src/field_theory/minimal_polynomial.lean : line 319 : 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
src/field_theory/splitting_field.lean : line 15 : ERR_MOD : Module docstring missing, or too late
src/field_theory/splitting_field.lean : line 377 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 379 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 382 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 439 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 489 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 504 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 580 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 76 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 16 : ERR_MOD : Module docstring missing, or too late
src/field_theory/splitting_field.lean : line 378 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 380 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 383 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 440 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 490 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 505 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 581 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 77 : ERR_LIN : Line has more than 100 characters
src/field_theory/splitting_field.lean : line 78 : ERR_LIN : Line has more than 100 characters
src/field_theory/subfield.lean : line 449 : ERR_LIN : Line has more than 100 characters
src/geometry/euclidean/basic.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/geometry/euclidean/basic.lean : line 196 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1206,12 +1206,12 @@ src/number_theory/primorial.lean : line 138 : ERR_LIN : Line has more than 100 c
src/number_theory/primorial.lean : line 146 : ERR_LIN : Line has more than 100 characters
src/number_theory/primorial.lean : line 147 : ERR_LIN : Line has more than 100 characters
src/number_theory/primorial.lean : line 39 : ERR_LIN : Line has more than 100 characters
src/number_theory/pythagorean_triples.lean : line 179 : ERR_LIN : Line has more than 100 characters
src/number_theory/pythagorean_triples.lean : line 283 : ERR_LIN : Line has more than 100 characters
src/number_theory/pythagorean_triples.lean : line 180 : ERR_LIN : Line has more than 100 characters
src/number_theory/pythagorean_triples.lean : line 284 : ERR_LIN : Line has more than 100 characters
src/number_theory/pythagorean_triples.lean : line 315 : ERR_LIN : Line has more than 100 characters
src/number_theory/pythagorean_triples.lean : line 419 : ERR_LIN : Line has more than 100 characters
src/number_theory/pythagorean_triples.lean : line 82 : ERR_LIN : Line has more than 100 characters
src/number_theory/pythagorean_triples.lean : line 285 : ERR_LIN : Line has more than 100 characters
src/number_theory/pythagorean_triples.lean : line 316 : ERR_LIN : Line has more than 100 characters
src/number_theory/pythagorean_triples.lean : line 420 : ERR_LIN : Line has more than 100 characters
src/number_theory/pythagorean_triples.lean : line 83 : ERR_LIN : Line has more than 100 characters
src/number_theory/quadratic_reciprocity.lean : line 443 : ERR_LIN : Line has more than 100 characters
src/number_theory/sum_four_squares.lean : line 21 : ERR_MOD : Module docstring missing, or too late
src/order/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -1480,11 +1480,11 @@ src/tactic/group.lean : line 36 : ERR_LIN : Line has more than 100 characters
src/tactic/hint.lean : line 57 : ERR_LIN : Line has more than 100 characters
src/tactic/hint.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/induction.lean : line 1252 : ERR_RNT : Reserved notation outside tactic.reserved_notation
src/tactic/interactive.lean : line 1117 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive.lean : line 1057 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive.lean : line 379 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive.lean : line 703 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive.lean : line 643 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive.lean : line 846 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/interactive.lean : line 906 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 153 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 173 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 177 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit ca2e536

Please sign in to comment.