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

I am happy to remove some nolints for you!
leanprover-community · Nov 5, 2022 · 22fe10d · 22fe10d
1 parent 9726554
commit 22fe10d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -208,7 +208,7 @@ apply_nolint matrix.induction_on' fintype_finite
 -- data/multiset/functor.lean
 apply_nolint multiset.traverse doc_blame
 
--- data/nat/basic.lean
+-- data/nat/order.lean
 apply_nolint nat.subtype.order_bot fails_quickly
 
 -- data/num/bitwise.lean