Code

Get position#281

Code

Open

javier-m wants to merge 2 commits intoleanprover:masterleanprover/vscode-lean:masterfrom timlacroix:get-positiontimlacroix/vscode-lean:get-positionCopy head branch name to clipboard

+20-6

Commits

Commits on Sep 27, 2021

• export infoView API

  

  Timothee Lacroix

  committed
  3293311

  Copy full SHA for 3293311

Commits on Oct 12, 2021

• pass widget as callback arg

  javier-m

  committed
  1290949

  Copy full SHA for 1290949