From e048bbc93a95533f2f0746cfcc9b948e5a2c1722 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 28 Jul 2022 15:20:26 +0200
Subject: [PATCH] perf: unused variables linter: early cut-off

---
 src/Lean/Linter/UnusedVariables.lean | 3 +++
 1 file changed, 3 insertions(+)

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