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

I am happy to remove some nolints for you!
leanprover-community · Oct 14, 2022 · 8f9520e · 8f9520e
1 parent 1e9b3df
commit 8f9520e
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -67,8 +67,6 @@ apply_nolint monoid.mfoldr.of_free_monoid doc_blame
 apply_nolint traversable.fold_map doc_blame
 apply_nolint traversable.foldl doc_blame
 apply_nolint traversable.foldr doc_blame
-apply_nolint traversable.free.map doc_blame
-apply_nolint traversable.free.mk doc_blame
 apply_nolint traversable.length doc_blame
 apply_nolint traversable.map_fold doc_blame
 apply_nolint traversable.mfoldl doc_blame