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

I am happy to remove some nolints for you!
leanprover-community · Dec 10, 2021 · e7959fb · e7959fb
1 parent 1ecdf71
commit e7959fb
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -406,9 +406,6 @@ apply_nolint relator.lift_fun doc_blame
 apply_nolint relator.right_total doc_blame
 apply_nolint relator.right_unique doc_blame
 
--- measure_theory/function/conditional_expectation.lean
-apply_nolint measure_theory.Lp_meas.complete_space fails_quickly
-
 -- meta/coinductive_predicates.lean
 apply_nolint monotonicity doc_blame
 apply_nolint tactic.add_coinductive_predicate doc_blame