Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#3302)
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 7, 2020
1 parent f548db4 commit d62e71d
Showing 1 changed file with 4 additions and 6 deletions.
10 changes: 4 additions & 6 deletions scripts/nolints.txt
Expand Up @@ -62,7 +62,6 @@ apply_nolint linear_ordered_field doc_blame
-- algebra/ring.lean
apply_nolint comm_ring doc_blame
apply_nolint comm_semiring doc_blame
apply_nolint distrib doc_blame
apply_nolint integral_domain doc_blame
apply_nolint ring doc_blame
apply_nolint ring_hom has_inhabited_instance
Expand Down Expand Up @@ -2251,6 +2250,10 @@ apply_nolint continuous_map.compact_open.gen doc_blame
apply_nolint continuous_map.ev doc_blame
apply_nolint continuous_map.induced doc_blame

-- topology/compacts.lean
apply_nolint topological_space.closeds has_inhabited_instance
apply_nolint topological_space.nonempty_compacts has_inhabited_instance

-- topology/homeomorph.lean
apply_nolint homeomorph has_inhabited_instance

Expand Down Expand Up @@ -2284,11 +2287,6 @@ apply_nolint isometric has_inhabited_instance
apply_nolint premetric_space doc_blame

-- topology/opens.lean
apply_nolint continuous.comap doc_blame
apply_nolint topological_space.closeds has_inhabited_instance
apply_nolint topological_space.nonempty_compacts has_inhabited_instance
apply_nolint topological_space.opens.gi doc_blame
apply_nolint topological_space.opens.interior doc_blame
apply_nolint topological_space.opens.is_basis doc_blame

-- topology/sheaves/presheaf.lean
Expand Down

0 comments on commit d62e71d

Please sign in to comment.