Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#2403)
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 13, 2020
1 parent 51f7319 commit ca98659
Showing 1 changed file with 1 addition and 6 deletions.
7 changes: 1 addition & 6 deletions scripts/nolints.txt
Expand Up @@ -111,12 +111,7 @@ apply_nolint lie_subalgebra has_inhabited_instance
apply_nolint lie_submodule has_inhabited_instance

-- algebra/module.lean
apply_nolint ideal doc_blame
apply_nolint is_linear_map doc_blame
apply_nolint linear_map doc_blame
apply_nolint module.End doc_blame
apply_nolint module.core doc_blame has_inhabited_instance
apply_nolint submodule.subtype doc_blame
apply_nolint module.core has_inhabited_instance

-- algebra/order.lean
apply_nolint decidable.lt_by_cases doc_blame
Expand Down

0 comments on commit ca98659

Please sign in to comment.