Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#2436)
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 Apr 17, 2020
1 parent 0567b7f commit 715be9f
Showing 1 changed file with 0 additions and 6 deletions.
6 changes: 0 additions & 6 deletions scripts/nolints.txt
Expand Up @@ -564,12 +564,6 @@ apply_nolint category_theory.monad.comparison_forget doc_blame
apply_nolint category_theory.monad.algebra has_inhabited_instance
apply_nolint category_theory.monad.algebra.hom has_inhabited_instance

-- category_theory/monad/limits.lean
apply_nolint category_theory.has_limits_of_reflective doc_blame
apply_nolint category_theory.monad.forget_creates_limits.c doc_blame
apply_nolint category_theory.monad.forget_creates_limits.cone_point doc_blame
apply_nolint category_theory.monad.forget_creates_limits.γ doc_blame unused_arguments

-- category_theory/monoidal/functor.lean
apply_nolint category_theory.lax_monoidal_functor has_inhabited_instance
apply_nolint category_theory.monoidal_functor has_inhabited_instance
Expand Down

0 comments on commit 715be9f

Please sign in to comment.