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

I am happy to remove some nolints for you!
leanprover-community · Apr 23, 2020 · 0196748 · 0196748
1 parent fdbf22d
commit 0196748
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -3071,9 +3071,6 @@ apply_nolint tactic.split_ifs doc_blame
 -- tactic/subtype_instance.lean
 apply_nolint tactic.derive_field_subtype doc_blame
 
--- tactic/suggest.lean
-apply_nolint tactic.suggest.decl_data doc_blame
-
 -- tactic/tauto.lean
 apply_nolint tactic.add_edge doc_blame
 apply_nolint tactic.add_refl doc_blame