diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index 7efba9735b..2627cd5bd7 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -151,6 +151,9 @@ opaque getUnusedVariablesIgnoreFns : CommandElabM (Array IgnoreFunction) def unusedVariables : Linter := fun cmdStx => do + unless getLinterUnusedVariables (← getOptions) do + return + -- NOTE: `messages` is local to the current command if (← get).messages.hasErrors then return