Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5873)
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 Jan 25, 2021
1 parent 507c7ff commit 87202fe
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions scripts/style-exceptions.txt
Original file line number Diff line number Diff line change
Expand Up @@ -79,8 +79,8 @@ src/algebraic_geometry/sheafed_space.lean : line 82 : ERR_LIN : Line has more th
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 790 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 205 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 520 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 260 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 605 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/deriv.lean : line 1105 : ERR_LIN : Line has more than 100 characters
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
Expand Down Expand Up @@ -671,7 +671,7 @@ src/data/seq/computation.lean : line 11 : ERR_MOD : Module docstring missing, or
src/data/seq/parallel.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/data/seq/seq.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/seq/wseq.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/set/basic.lean : line 2400 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 2404 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 474 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 559 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 668 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1561,7 +1561,7 @@ src/topology/sheaves/sheaf_of_functions.lean : line 168 : ERR_LIN : Line has mor
src/topology/sheaves/stalks.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/topology/sheaves/stalks.lean : line 128 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/stalks.lean : line 133 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 811 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 840 : ERR_LIN : Line has more than 100 characters
src/topology/tactic.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/topology/topological_fiber_bundle.lean : line 135 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/absolute_value.lean : line 71 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 87202fe

Please sign in to comment.