chore(scripts): update nolints.txt (leanprover-community#3206)

I am happy to remove some nolints for you!
cipher1024 · Mar 15, 2022 · 53d886d · 53d886d
1 parent c840ce4
commit 53d886d
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -1900,9 +1900,6 @@ apply_nolint tactic.get_lift_prf doc_blame
 apply_nolint tactic.to_texpr doc_blame
 apply_nolint tactic.using_texpr doc_blame
 
--- tactic/linarith/lemmas.lean
-apply_nolint linarith.mul_eq unused_arguments
-
 -- tactic/local_cache.lean
 apply_nolint tactic.local_cache.internal.block_local.clear doc_blame
 apply_nolint tactic.local_cache.internal.block_local.get_name doc_blame