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

I am happy to remove some nolints for you!
leanprover-community · May 11, 2020 · a87f326 · a87f326
1 parent e777d0b
commit a87f326
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -1484,9 +1484,7 @@ apply_nolint hyperreal.pos_of_infinite_pos ge_or_gt
 apply_nolint nnreal.of_real doc_blame
 
 -- data/real/pi.lean
-apply_nolint real.pi_gt_314 ge_or_gt
 apply_nolint real.pi_gt_sqrt_two_add_series ge_or_gt
-apply_nolint real.pi_gt_three ge_or_gt
 apply_nolint real.sqrt_two_add_series_nonneg ge_or_gt
 apply_nolint real.sqrt_two_add_series_zero_nonneg ge_or_gt