Skip to content

v0.0.124

Choose a tag to compare

@github-actions github-actions released this 17 Jan 11:00
· 430 commits to master since this release
  • Make word-based occurrence highlighting fallback optional and set the default to disable it, c.f. #377 (Author: @david-christiansen)
  • Make InfoView colors configurable (Author: @david-christiansen)
  • Allow downloading projects with SSH Git links
  • Add the following abbreviations: average: ⨍, -int: ⨍, oiint: ∯, tint: ∯, pd: ∂ (Author: @girving)
  • Add red syntactic highlighting for sorry-like identifiers (admit, stop)
  • Display a modal warning before updating in the 'Update Dependency' command
  • Change label of 'Rebuild Imports' to 'Restart File' so that it is clear that they are the same thing
  • Adjust setup guide to move the description of what Lean depends on to the front