chore(scripts): update nolints.txt (#9895)

I am happy to remove some nolints for you!
leanprover-community · Oct 23, 2021 · 45ba2ad · 45ba2ad
1 parent 7690e0a
commit 45ba2ad
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -921,9 +921,6 @@ apply_nolint topological_space.open_nhds.map doc_blame
 -- topology/category/TopCommRing.lean
 apply_nolint TopCommRing has_inhabited_instance
 
--- topology/maps.lean
-apply_nolint inducing doc_blame
-
 -- topology/sheaves/presheaf.lean
 apply_nolint Top.presheaf has_inhabited_instance