Code

feat: shift-click to unselect#451

Code

Merged

Vtec234 merged 7 commits intomasterleanprover/vscode-lean4:masterfrom shift-unclickleanprover/vscode-lean4:shift-unclickCopy head branch name to clipboardJan 13, 2025

+198-138

Commits

Commits on Jan 12, 2025

• feat: selection via context menu

  Vtec234

  committed
  7725ba0

  Copy full SHA for 7725ba0

• chore: bump infoview and infoview-api versions

  Vtec234

  committed
  9b6d25d

  Copy full SHA for 9b6d25d

Commits on Jan 13, 2025

• feat: address review

  Vtec234

  committed
  460df9f

  Copy full SHA for 460df9f

• fix: remove auto-selection

  Vtec234

  committed
  8a9fe03

  Copy full SHA for 8a9fe03

• fix: hide tooltips on contextmenu

  Vtec234

  committed
  9bfb002

  Copy full SHA for 9bfb002

• chore: silence audit warning

  Vtec234

  committed
  829af4b

  Copy full SHA for 829af4b

• chore: update current-release

  Vtec234

  committed
  07e5f34

  Copy full SHA for 07e5f34