Zulip Chat Archive
Stream: new members
Topic: VSCode multiple cursor
Anatole Dedecker (Aug 09 2020 at 20:19):
Is it voluntary that we can't type unicode characters using \... while in multiple cursor mode in VSCode ?
Mario Carneiro (Aug 09 2020 at 20:19):
no
Bryan Gin-ge Chen (Aug 09 2020 at 20:20):
There's an open issue: https://github.com/leanprover/vscode-lean/issues/160
Presumably it's fixable but no one has had the time to yet.
Anatole Dedecker (Aug 09 2020 at 20:21):
Ok thanks !
Bryan Gin-ge Chen (Aug 11 2020 at 14:29):
Update: thanks to @Alex Peattie, version 0.16.7 of vscode-lean now supports Unicode input with multiple cursors!
Anatole Dedecker (Aug 11 2020 at 14:30):
Wow great news !
Kevin Buzzard (Aug 11 2020 at 17:04):
That's great! This has annoyed me forever and was annoying me over the weekend.
Last updated: Dec 20 2023 at 11:08 UTC