Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#6090)
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 Feb 8, 2021
1 parent 5bf92e1 commit 6b83e72
Showing 1 changed file with 9 additions and 9 deletions.
18 changes: 9 additions & 9 deletions scripts/style-exceptions.txt
Expand Up @@ -23,12 +23,12 @@ src/analysis/calculus/deriv.lean : line 1125 : ERR_LIN : Line has more than 100
src/analysis/calculus/local_extr.lean : line 22 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/local_extr.lean : line 305 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/tangent_cone.lean : line 250 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 1402 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 1813 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 2452 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 2470 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 689 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 846 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 1423 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 1834 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 2473 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 2491 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 710 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/times_cont_diff.lean : line 867 : ERR_LIN : Line has more than 100 characters
src/analysis/complex/polynomial.lean : line 50 : ERR_LIN : Line has more than 100 characters
src/analysis/convex/caratheodory.lean : line 76 : ERR_LIN : Line has more than 100 characters
src/analysis/convex/extrema.lean : line 96 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -524,9 +524,9 @@ src/linear_algebra/matrix.lean : line 711 : ERR_LIN : Line has more than 100 cha
src/linear_algebra/matrix.lean : line 724 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/matrix.lean : line 865 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/special_linear_group.lean : line 53 : ERR_LIN : Line has more than 100 characters
src/logic/function/basic.lean : line 338 : ERR_LIN : Line has more than 100 characters
src/logic/function/basic.lean : line 527 : ERR_LIN : Line has more than 100 characters
src/logic/function/basic.lean : line 567 : ERR_LIN : Line has more than 100 characters
src/logic/function/basic.lean : line 352 : ERR_LIN : Line has more than 100 characters
src/logic/function/basic.lean : line 541 : ERR_LIN : Line has more than 100 characters
src/logic/function/basic.lean : line 581 : ERR_LIN : Line has more than 100 characters
src/logic/relation.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/category/Meas.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand Down

0 comments on commit 6b83e72

Please sign in to comment.