Code

fix: broken create project command#412

Code

Merged

mhuisi merged 1 commit intoleanprover:masterleanprover/vscode-lean4:masterfrom mhuisi:mhuisi/project-init-lake-check-bugmhuisi/vscode-lean4:mhuisi/project-init-lake-check-bugCopy head branch name to clipboardMar 19, 2024

+4-4

Commits

Commits on Mar 19, 2024

• fix: broken create project command

  mhuisi

  committed
  d27b152

  Copy full SHA for d27b152