Skip to content

Commit 497e3b3

Browse files
leanprover-community-botgithub-actions[bot]
authored andcommitted
chore(scripts): update nolints.json
1 parent 1825e17 commit 497e3b3

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)