VS Code issues

Stream: new members

[Dominique Danco]

I've been having some sketchy behavior with the VS code extension. Sometimes when I open my project, the Lean server will fail to start, and I am occasionally told to install Lean (which is already installed). If I close and restart the folder a few times, it usually eventually starts working properly.

Has anyone seen behavior like this before, or know how to fix it? Thanks

[Xiyu Zhai]

I had this on windows.