WS connections not closed

[joneugster]

Report by the Lean FRO:

I am observing a possible bug with lean4web: If I am open, for example, https://lean.math.hhu.de/#project=nightly&codez=M4EwZkA
and look at the network tab of the Firefox debug console I see two open WS connections, one to the default project (mathlib-demo) and one to the selected one, and both seem to be active. I also noticed duplicated worker processes on the server.

[nomeata]

It seems that as consequence of this bug one can see diagnostics (squiggly lies) from the default version and error messages from the selected version, see
leanprover/lean4#6034 (comment)

@joneugster, what is the status of this issue?