VS Code: copy from Lean messages

Stream: new members

[Alexander Bentkamp]

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]

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]

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]

I have this problem, too.

[Johan Commelin]

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

[Johan Commelin]

I'm also not using Windows...

[Chris Hughes]

I have this problem on mac.