max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: "linting" profiler metric

Browse source
This commit is contained in:
Sebastian Ullrich 2022-07-07 14:22:25 +02:00
parent 29bdc0ceac
commit 305866dba2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Command.lean
View file

@ -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