Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#6213)
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 13, 2021
1 parent 37459ee commit 5869039
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions scripts/style-exceptions.txt
Expand Up @@ -992,9 +992,8 @@ 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 827 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 846 : 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
src/topology/uniform_space/compact_separated.lean : line 128 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/separation.lean : line 305 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 5869039

Please sign in to comment.