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

I am happy to remove some nolints for you!
leanprover-community · Aug 28, 2021 · d3c592f · d3c592f
1 parent 0fd51b1
commit d3c592f
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -390,7 +390,6 @@ apply_nolint function.embedding.Pi_congr_right doc_blame
 apply_nolint function.embedding.arrow_congr_left doc_blame
 apply_nolint function.embedding.arrow_congr_right doc_blame
 apply_nolint function.embedding.congr doc_blame
-apply_nolint function.embedding.of_not_nonempty doc_blame
 apply_nolint function.embedding.refl doc_blame
 apply_nolint function.embedding.subtype_map doc_blame
 apply_nolint function.embedding.trans doc_blame