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: Feb 28 2026 at 14:05 UTC