Zulip Chat Archive
Stream: general
Topic: How to open VSCode-Lean files?
Daniel Donnelly (Aug 28 2019 at 06:10):
I tried VSCode > File > Open Folder > vscode-lean > select folder
and VSCode crashed.
Daniel Donnelly (Aug 28 2019 at 06:11):
Got it to work, just restarted VSCode and tried again.
Last updated: Dec 20 2023 at 11:08 UTC