Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#15582)
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 21, 2022
1 parent 6b34a40 commit b5e9ffd
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion scripts/nolints.txt
Expand Up @@ -1080,7 +1080,7 @@ apply_nolint cardinal.mk_compl_eq_mk_compl_finite_same fintype_finite
-- set_theory/lists.lean
apply_nolint finsets doc_blame

-- set_theory/zfc.lean
-- set_theory/zfc/basic.lean
apply_nolint Set.map_definable_aux unused_arguments

-- tactic/abel.lean
Expand Down

0 comments on commit b5e9ffd

Please sign in to comment.