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

I am happy to remove some nolints for you!
leanprover-community · Sep 27, 2020 · 5f6b07f · 5f6b07f
1 parent 5c957ec
commit 5f6b07f
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -1815,7 +1815,6 @@ apply_nolint topological_space.opens.is_basis doc_blame
 
 -- topology/sheaves/presheaf.lean
 apply_nolint Top.presheaf doc_blame has_inhabited_instance
-apply_nolint Top.presheaf.pushforward doc_blame
 apply_nolint Top.presheaf.pushforward.comp doc_blame
 apply_nolint Top.presheaf.pushforward.id doc_blame
 apply_nolint Top.presheaf.pushforward_eq doc_blame