diff --git a/test/lint_unreachableTactic.lean b/test/lint_unreachableTactic.lean index 8526b616df..733f62832f 100644 --- a/test/lint_unreachableTactic.lean +++ b/test/lint_unreachableTactic.lean @@ -1,5 +1,12 @@ import Batteries.Linter.UnreachableTactic +-- The warning generated by `linter.unreachableTactic` is not suppressed by `#guard_msgs`, +-- because the linter is run on `#guard_msgs` itself. This is a known issue, see +-- https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/unreachableTactic.20linter.20not.20suppressed.20by.20.60.23guard_msgs.60 +-- We jump through an extra hoop here to silence the warning. +set_option linter.unreachableTactic false in +#guard_msgs(drop warning) in +set_option linter.unreachableTactic true in /-- warning: this tactic is never executed note: this linter can be disabled with `set_option linter.unreachableTactic false`