Skip to content

Commit 9dc3933

Browse files
chore(scripts): update nolints.json (leanprover-community#39761)
I am happy to remove some nolints for you!
1 parent 878dc46 commit 9dc3933

1 file changed

Lines changed: 0 additions & 1 deletion

File tree

scripts/nolints.json

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,6 @@
144144
["defsWithUnderscore", "Finite.divisionRing_to_field"],
145145
["defsWithUnderscore", "Finset.instGradeMinOrder_multiset"],
146146
["defsWithUnderscore", "Finset.instGradeMinOrder_nat"],
147-
["defsWithUnderscore", "Finsupp.onFinset_support"],
148147
["defsWithUnderscore", "FixedDetMatrices.reduce_rec"],
149148
["defsWithUnderscore", "FractionRing.mulSemiringAction_of_isGaloisGroup"],
150149
["defsWithUnderscore", "Function.fromTypes_cons_equiv"],

0 commit comments

Comments
 (0)