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: May 02 2025 at 03:31 UTC