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

I am happy to remove some nolints for you!
leanprover-community · May 17, 2020 · a206df1 · a206df1
1 parent b530cdb
commit a206df1
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -1643,7 +1643,6 @@ apply_nolint mul_action.orbit doc_blame
 apply_nolint mul_action.orbit_equiv_quotient_stabilizer doc_blame
 apply_nolint mul_action.orbit_rel doc_blame
 apply_nolint mul_action.stabilizer doc_blame
-apply_nolint mul_action.to_perm doc_blame
 
 -- group_theory/order_of_element.lean
 apply_nolint exists_pow_eq_one ge_or_gt