chore(scripts): update nolints.txt

leanprover-community · Mar 19, 2020 · 034685b · 034685b
1 parent 00d9f1d
commit 034685b
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -198,7 +198,6 @@ apply_nolint algebraic_geometry.PresheafedSpace.stalk_map doc_blame
 
 -- analysis/normed_space/basic.lean
 apply_nolint normed_group.tendsto_nhds_zero ge_or_gt
-apply_nolint summable_iff_vanishing_norm ge_or_gt
 
 -- analysis/normed_space/real_inner_product.lean
 apply_nolint has_inner doc_blame
@@ -3515,9 +3514,6 @@ apply_nolint homeomorph.mul_left doc_blame
 apply_nolint homeomorph.mul_right doc_blame
 apply_nolint homeomorph.neg doc_blame
 
--- topology/algebra/infinite_sum.lean
-apply_nolint option.cases_on' doc_blame
-
 -- topology/algebra/module.lean
 apply_nolint continuous_linear_equiv has_inhabited_instance