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

I am happy to remove some nolints for you!
leanprover-community · Apr 26, 2020 · c34add7 · c34add7
1 parent bda206a
commit c34add7
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -1261,9 +1261,6 @@ apply_nolint multiset.traverse doc_blame
 -- data/nat/enat.lean
 apply_nolint enat doc_blame
 
--- data/nat/modeq.lean
-apply_nolint nat.modeq.chinese_remainder doc_blame
-
 -- data/nat/prime.lean
 apply_nolint nat.min_fac_aux doc_blame