pull/204/head
Jon Eugster 2 years ago
parent 87689e1c3a
commit e07570181c

@ -192,7 +192,7 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B
-- so showing the message "intermediate goal solved" would be confusing. -- so showing the message "intermediate goal solved" would be confusing.
if (¬ (filterUnsolvedGoal startDiags).any (·.severity? == some .error)) then if (¬ (filterUnsolvedGoal startDiags).any (·.severity? == some .error)) then
out := out.push { out := out.push {
message := .text "intermediate goal solved :(! 🎉" message := .text "intermediate goal solved! 🎉"
range := { range := {
start := pos start := pos
«end» := pos «end» := pos

Loading…
Cancel
Save