chore(scripts): update nolints.txt

leanprover-community · Mar 25, 2020 · 05aa955 · 05aa955
1 parent bedb810
commit 05aa955
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -2190,7 +2190,6 @@ apply_nolint relator.right_unique doc_blame
 
 -- logic/unique.lean
 apply_nolint unique doc_blame
-apply_nolint unique.of_surjective doc_blame
 
 -- measure_theory/ae_eq_fun.lean
 apply_nolint measure_theory.ae_eq_fun.add doc_blame