Skip to content

v0.0.230-pre

Pre-release
Pre-release

Choose a tag to compare

@github-actions github-actions released this 01 Apr 08:06
· 32 commits to master since this release
  • Ensure that redundant redundant interactive requests are canceled (#746, author: @Vtec234)
  • Fix a bug where some commands would sometimes try to execute in the wrong project (#750)
  • Add file icons for .lean files (#749)
  • Improve progress bar messages when downloading a project (#748)