v0.0.170
·
87 commits
to master
since this release
- Fix a bug that would sometimes crash the extension on activation (vscode-lean4#488)
- Ensure that the "Internal error" popup at the start is not excessively large (vscode-lean4#488)