vscode-lean icon indicating copy to clipboard operation
vscode-lean copied to clipboard
verified publisher icon leanprover

Live Share

Open bryangingechen opened this issue 5 years ago • 1 comments

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Sever.20sharing.20in.20live.20share/near/202056350

I can try to take a crack at this after the widget refactor settles.

bryangingechen avatar Jun 26 '20 06:06 bryangingechen

:beer: :beer: :beer:

jcommelin avatar Jun 26 '20 07:06 jcommelin