Skip to content

Commit d0c5d20

Browse files
leanprover-community-bot-assistantleanprover-community-bot
andcommitted
chore(scripts): update nolints.json (#32859)
I am happy to remove some nolints for you! [workflow run for this PR](https://github.com/leanprover-community/mathlib4/actions/runs/20199788622) Co-authored-by: leanprover-community-bot <leanprover.community@gmail.com>
1 parent 1825e17 commit d0c5d20

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

scripts/nolints.json

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,6 @@
169169
["docBlame", "Mathlib.Notation3.prettyPrintOpt"],
170170
["docBlame", "Mathlib.Tactic.evalIntrov"],
171171
["docBlame", "Mathlib.Tactic.setArgsRest"],
172-
["docBlame", "Mathlib.Tactic.tacticMatch_target_"],
173172
["docBlame", "Mathlib.Tactic.usingArg"],
174173
["docBlame", "Mathlib.Tactic.withArgs"],
175174
["docBlame", "Mathlib.WhatsNew.diffExtension"],

0 commit comments

Comments
 (0)