Skip to content

v0.0.225

Choose a tag to compare

View all tags
@mhuisi mhuisi released this 05 Mar 12:44
· 27 commits to master since this release
v0.0.225
27f5b36
  • Add a "Copy Module Name" command to the context menu for Lean editor tabs (#717)
  • Fix several bugs related to syntax highlighting markdown in comments (#711)
  • Fix a bug in the InfoView where it constantly unnecessarily displayed a scroll bar (#721, author: @quartztz)
  • Fix a bug in the unicode input web component (used in the LoogleView) where inputting \to\to would only expand one of the abbreviations (#718)
  • Change the "Proceed" labels of some dialogs to "Proceed Regardless" to reduce confusion (#715)
  • Remove two buggy alternative abbreviations: \c[ for ⦃ (default: \{{) and \c] for ⦄ (default: \}}) (#710)
  • Fix bug where abbreviations including backticks were not displayed correctly in hover tooltips (#709)

(Release created manually due to an issue with CI)

Contributors

quartztz
Assets 3
Loading