Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#9475)
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 Oct 1, 2021
1 parent 125dac8 commit 812d6bb
Showing 1 changed file with 0 additions and 9 deletions.
9 changes: 0 additions & 9 deletions scripts/style-exceptions.txt
@@ -1,14 +1,8 @@
src/category_theory/adjunction/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/adjunction/fully_faithful.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/adjunction/limits.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/endomorphism.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/category_theory/epi_mono.lean : line 15 : ERR_MOD : Module docstring missing, or too late
src/category_theory/eq_to_hom.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/full_subcategory.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/fully_faithful.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/functor.lean : line 18 : ERR_MOD : Module docstring missing, or too late
src/category_theory/functor_category.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/groupoid.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/cones.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/creates.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/functor_category.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Expand All @@ -18,10 +12,7 @@ src/category_theory/limits/shapes/finite_products.lean : line 10 : ERR_MOD : Mod
src/category_theory/limits/types.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/monad/adjunction.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/monad/basic.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/natural_transformation.lean : line 16 : ERR_MOD : Module docstring missing, or too late
src/category_theory/opposites.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/products/bifunctor.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/whiskering.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/computability/partrec_code.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/control/applicative.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/control/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Expand Down

0 comments on commit 812d6bb

Please sign in to comment.