vscode-lean icon indicating copy to clipboard operation
vscode-lean copied to clipboard

(WIP) add insertGoal command

Open bryangingechen opened this issue 5 years ago • 0 comments

As requested on Zulip

bryangingechen avatar Nov 14 '20 17:11 bryangingechen