Code

Rename "Install Elan" button#356

Code

Merged

mhuisi merged 1 commit intoleanprover:masterleanprover/vscode-lean4:masterfrom mhuisi:mhuisi/install-elan-button-namemhuisi/vscode-lean4:mhuisi/install-elan-button-nameCopy head branch name to clipboardNov 14, 2023

+4-4

Commits

Commits on Nov 10, 2023

• chore: rename "install elan" button

  mhuisi

  committed
  4359b11

  Copy full SHA for 4359b11