Ali Caglayan (Jul 14 2021 at 14:11): Ali Caglayan (Jul 14 2021 at 14:11):Can anyone confirm that the zoom in shortcut Ctrl + + actually works in coqide? I haven't been able to get it to work and I am wondering if it is something on my end.
Michael Soegtrop (Jul 14 2021 at 17:04):Doesn't work for me on Mac either. The menu function works, though.
Jim Fehrle (Jul 14 2021 at 21:52):It works for me, but I have to hold the Shift key in addition since + is a shifted character on my US-style keyboard
Ali Caglayan (Jul 14 2021 at 23:20):It is working!
Ali Caglayan (Jul 14 2021 at 23:20):Thanks @Jim Fehrle
Ali Caglayan (Jul 14 2021 at 23:20):It's strange that the keyboard locale isn't taken into account
Last updated: Oct 13 2024 at 01:02 UTC