Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#17703)
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 Nov 24, 2022
1 parent 364d871 commit 6b3325c
Showing 1 changed file with 0 additions and 3 deletions.
3 changes: 0 additions & 3 deletions scripts/nolints.txt
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,6 @@ apply_nolint free_algebra.semiring check_reducibility
-- category_theory/limits/filtered_colimit_commutes_finite_limit.lean
apply_nolint category_theory.limits.colimit_limit_to_limit_colimit_is_iso fails_quickly

-- category_theory/limits/shapes/finite_products.lean
apply_nolint category_theory.limits.has_fintype_coproducts fintype_finite

-- computability/partrec.lean
apply_nolint computable doc_blame
apply_nolint computable₂ doc_blame
Expand Down

0 comments on commit 6b3325c

Please sign in to comment.