Skip to content

v0.0.118

Choose a tag to compare

View all tags
@github-actions github-actions released this 31 Oct 17:31
· 463 commits to master since this release
v0.0.118
2f3f44e
  • Remove the server restart prompt after discussion on Zulip
  • Change name of lean4.createMathlibProject to be easier to understand
  • Ensure that "Restart File" (Ctrl+Shift+X) does not open the extensions menu anymore when in a Lean 4 context
  • Make "Toggle Infoview" and "Toggle All Messages" keybindings work when not focusing the editor window
  • Ensure that commands displayed in command pallette are independent of focused part of VS Code
  • Fix Lean server crashing with bad error message when no default toolchain is set because it was uninstalled in the past
Assets 3
Loading