Skip to content

Commit

Permalink
chore(scripts): update nolints.txt
Browse files Browse the repository at this point in the history
  • Loading branch information
leanprover-community-bot committed Feb 28, 2020
1 parent 4637e5c commit 0bf2064
Showing 1 changed file with 0 additions and 3 deletions.
3 changes: 0 additions & 3 deletions scripts/nolints.txt
Original file line number Diff line number Diff line change
Expand Up @@ -233,9 +233,6 @@ apply_nolint prime_spectrum has_inhabited_instance
apply_nolint algebraic_geometry.PresheafedSpace.stalk doc_blame
apply_nolint algebraic_geometry.PresheafedSpace.stalk_map doc_blame

-- analysis/calculus/times_cont_diff.lean
apply_nolint times_cont_diff.times_cont_diff_fderiv_apply unused_arguments

-- analysis/normed_space/basic.lean
apply_nolint normed_group.tendsto_nhds_zero ge_or_gt
apply_nolint summable_iff_vanishing_norm ge_or_gt
Expand Down

0 comments on commit 0bf2064

Please sign in to comment.