Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#15685)
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 Jul 26, 2022
1 parent 1142e0b commit df09f2a
Showing 1 changed file with 0 additions and 4 deletions.
4 changes: 0 additions & 4 deletions scripts/nolints.txt
Expand Up @@ -893,10 +893,6 @@ apply_nolint is_countably_spanning.pi fintype_finite
apply_nolint measure_theory.measure.prod_sum fintype_finite
apply_nolint measure_theory.measure.sum_prod fintype_finite

-- measure_theory/function/uniform_integrable.lean
apply_nolint measure_theory.unif_integrable_fintype fintype_finite
apply_nolint measure_theory.uniform_integrable_fintype fintype_finite

-- measure_theory/group/prod.lean
apply_nolint measure_theory.map_prod_inv_mul_eq to_additive_doc
apply_nolint measure_theory.map_prod_inv_mul_eq_swap to_additive_doc
Expand Down

0 comments on commit df09f2a

Please sign in to comment.