Skip to content

Commit e65f5f1

Browse files
mhuisikim-em
authored andcommitted
fix: broken goals accomplished (#8242)
This PR fixes the 'goals accomplished' diagnostics. They were accidentally broken in #7902. Regression test tbd in a future PR. (cherry picked from commit 65b37b4)
1 parent 2525330 commit e65f5f1

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Lean/Elab/MutualDef.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1165,7 +1165,7 @@ is error-free and contains no syntactical `sorry`s.
11651165
-/
11661166
private def logGoalsAccomplishedSnapshotTask (views : Array DefView)
11671167
(defsParsedSnap : DefsParsedSnapshot) : TermElabM Unit := do
1168-
if Lean.Elab.inServer.get (← getOptions) then
1168+
if ! Lean.Elab.inServer.get (← getOptions) then
11691169
-- Skip 'goals accomplished' task if we are on the command line.
11701170
-- These messages are only used in the language server.
11711171
return

0 commit comments

Comments
 (0)