Quirky behavior in VSCode 1.103

Stream: lean4

[Klaus Gy]

Anyone else noticed the Lean 4 extension for VSCode becoming very quirky recently? On cmd+C, it sometimes jumps to the documentation, or to a different file, or to a different position in the current file (sometimes I feel it's about where my mouse hovers while I press the keys). Also often the selection (not the content) just vanishes without anything being copied. I noticed it on https://live.lean-lang.org too, I don't know if this is due to an update of the extension or due to an update to VSCode.

[Klaus Gy]

NVM this is a hardware problem :D

[Sebastian Ullrich]

Is the hardware in question a quantum device?

[Klaus Gy]

haha no, i realized that my thinkpad's left alt key somehow generates a left mouse click as well, which leads to all kind of quirks