Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore(scripts): update nolints.txt #17008

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore(scripts): update nolints.txt #17008

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 0 additions & 5 deletions scripts/nolints.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,11 +137,6 @@ apply_nolint tactic.interactive.traverse_constructor unused_arguments
apply_nolint tactic.interactive.traverse_field unused_arguments
apply_nolint tactic.interactive.with_prefix doc_blame

-- data/finset/noncomm_prod.lean
apply_nolint add_monoid_hom.pi_ext fintype_finite
apply_nolint finset.noncomm_prod_union_of_disjoint to_additive_doc
apply_nolint monoid_hom.pi_ext fintype_finite

-- data/finsupp/pwo.lean
apply_nolint finsupp.is_pwo fintype_finite

Expand Down