From 305866dba2eb609a81361a50ad21696d40831f5d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 7 Jul 2022 14:22:25 +0200 Subject: [PATCH] feat: "linting" profiler metric --- src/Lean/Elab/Command.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 41d099c714..f3c29074d1 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -190,7 +190,7 @@ instance : MonadLog CommandElabM where let msg := { msg with data := MessageData.withNamingContext { currNamespace := currNamespace, openDecls := openDecls } msg.data } modify fun s => { s with messages := s.messages.add msg } -def runLinters (stx : Syntax) : CommandElabM Unit := do +def runLinters (stx : Syntax) : CommandElabM Unit := do profileitM Exception "linting" (← getOptions) do let linters ← lintersRef.get unless linters.isEmpty do for linter in linters do