Code

Introduce issue templates#324

Code

Merged

mhuisi merged 1 commit intoleanprover:masterleanprover/vscode-lean4:masterfrom mhuisi:mhuisi/issue-templatesmhuisi/vscode-lean4:mhuisi/issue-templatesCopy head branch name to clipboardSep 15, 2023

+66

Commits

Commits on Sep 15, 2023

• chore: issue templates similar to lean4 repo

  mhuisi

  committed
  939dd78

  Copy full SHA for 939dd78