Skip to content

v0.0.223

Choose a tag to compare

@github-actions github-actions released this 09 Feb 12:18
· 80 commits to master since this release
  • Add support for nested Lean projects (#699)
  • Support cancellation of RPC requests (#700, author: @Vtec234)
  • Remove backtick name TextMate highlighting to fix false-positives (#692)
  • Ensure that editor is focused after edit (e.g. in a hint) (#702)
  • Change \<n abbreviation to \notlt (#685, author: @kckennylau)