Stream: new members
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.
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.
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.
Scott Morrison (May 08 2019 at 19:13):
I have this problem, too.
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.
Johan Commelin (May 08 2019 at 19:14):
I'm also not using Windows...
Chris Hughes (May 08 2019 at 19:14):
I have this problem on mac.
Last updated: May 11 2021 at 21:10 UTC