Unable to build vscode.lean

Stream: general

[Daniel Donnelly]

Hi. I've cloned the repository on git. I had it cloned and running before, except I need to start over fresh to get through some other bugs.

So starting fresh, I hit F5 to debug, and get the following:

pasted image

[Bryan Gin-ge Chen]

Did you rerun npm install?

[Daniel Donnelly]

Yep, thank you! That was the problem. :)

[Daniel Donnelly]

Got pretty far so far. It's official, VSCode is opening Bancats alongside Lean:
pasted image

[Jesse Michael Han]

(deleted)