Zulip Chat Archive

Stream: general

Topic: Unable to build vscode.lean


view this post on Zulip Daniel Donnelly (Aug 30 2019 at 16:58):

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

view this post on Zulip Bryan Gin-ge Chen (Aug 30 2019 at 17:14):

Did you rerun npm install?

view this post on Zulip Daniel Donnelly (Aug 30 2019 at 17:17):

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

view this post on Zulip Daniel Donnelly (Aug 30 2019 at 20:58):

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

view this post on Zulip Jesse Michael Han (Aug 31 2019 at 01:25):

(deleted)


Last updated: May 18 2021 at 17:44 UTC