Zulip Chat Archive

Stream: new members

Topic: VS Code: copy from Lean messages


view this post on Zulip Alexander Bentkamp (May 08 2019 at 16:05):

Does anyone else have problems copying text from the Lean Messages areas? If I try, VSCode doesn't react for a few seconds and usually the text does not end up in the clipboard. I am using VSCode on Mac OS.

view this post on Zulip Bryan Gin-ge Chen (May 08 2019 at 16:13):

I can reproduce this. It might be related to this VS code issue. One (annoying) workaround is to copy text using the "Copy" command in the "Edit" menu rather than using the keyboard shortcut.

view this post on Zulip Bryan Gin-ge Chen (May 08 2019 at 16:19):

Another workaround is the "Lean: Info View: Copy Contents to Comment" command, which you can access by typing cmd+shift+p and typing "lean". It can also be assigned a shortcut of its own.

view this post on Zulip Scott Morrison (May 08 2019 at 19:13):

I have this problem, too.

view this post on Zulip Johan Commelin (May 08 2019 at 19:13):

Is this a Mac thing? I don't have this problem... and I'm not using Mac.

view this post on Zulip Johan Commelin (May 08 2019 at 19:14):

I'm also not using Windows...

view this post on Zulip Chris Hughes (May 08 2019 at 19:14):

I have this problem on mac.


Last updated: May 11 2021 at 21:10 UTC