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

I am happy to remove some nolints for you!
leanprover-community · Oct 19, 2021 · 1ec385d · 1ec385d
1 parent 04094c4
commit 1ec385d
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -228,7 +228,6 @@ apply_nolint holor_index.drop doc_blame
 apply_nolint holor_index.take doc_blame
 
 -- data/list/defs.lean
-apply_nolint list.permutations_aux.rec doc_blame
 apply_nolint list.sublists'_aux doc_blame
 apply_nolint list.sublists_aux doc_blame
 apply_nolint list.sublists_aux₁ doc_blame