Got `shutdown` request, expected an `exit` notification

Stream: lean4

[Kevin Buzzard]

The following is pretty common for me: I have VS Code open (e.g. I'm reviewing a mathlib PR). I then switch branch on the command line, lake exe cache get, click the blue "restart lean" button in VS Code, get

Watchdog error: Got shutdown request, expected an exit notification

, ignore it, and everything is fine. Is this expected? I don't understand the error. Is it benign?

[Kim Morrison]

Yes, I get this too.

[Kim Morrison]

It looks like there simply isn't an issue for it, so it might not be on @Marc Huisinga's radar.

[Ruben Van de Velde]

I only saw that today for the first time, but yeah, doesn't seem like it's harmful