Goals accomplished diagnostics in 4.20

Stream: lean4

[Julian Berman]

I think Marc's on vacation so will ask here -- did goals accomplished diagnostics get backed out (removed) in 4.20? I don't see them being sent. I.e. example : 2 = 2 := by rfl on 4.19 shows a double checkmark in the VSCode gutter and "Goals accomplished" in the infoview, but I see neither on 4.20.

[Julian Berman]

Ah, maybe I see a PR which changed the behavior now at least...

[Marc Huisinga]

#8242

[Kevin Buzzard]

lean4#8242

[Kim Morrison]

Should be fixed in Mathlib at #24630.