chore: hide "show imports" and "show imported by" commands in command palette - #781

chore: hide "show imports" and "show imported by" commands in command palette#781

mhuisi merged 1 commit into

leanprover:masterleanprover/vscode-lean4:masterfrom

mhuisi:push-xywqqzouoksrmhuisi/vscode-lean4:push-xywqqzouoksrCopy head branch name to clipboard