Code

Use lean4 scope for lean-markdown#361

Code

Merged

mhuisi merged 1 commit intoleanprover:masterleanprover/vscode-lean4:masterfrom mhuisi:mhuisi/lean-markdown-scope-namemhuisi/vscode-lean4:mhuisi/lean-markdown-scope-nameCopy head branch name to clipboardNov 26, 2023

+10-10

Commits

Commits on Nov 22, 2023

• chore: use lean4 scope for lean-markdown

  mhuisi

  committed
  b6c544b

  Copy full SHA for b6c544b