Skip to content

v0.0.234

Choose a tag to compare

@github-actions github-actions released this 13 Apr 12:38
· 23 commits to master since this release
  • Split the 'Fetch Mathlib Build Cache For Current Imports' command into three (#757)
  • Ensure that 'Fetch Mathlib Build Cache For ...' commands can be used downstream of Mathlib (#757)
  • Add file icons for .lean files (#749, #753)
  • 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)
  • Fix a potential bug where closing the InfoView could yield an 'undefined' error (#756)
  • Improve progress bar messages when downloading a project (#748)