Stream: User interfaces devs & users

Topic: Zooming in shortcut Coqide


view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Jul 14 2021 at 17:04):

Doesn't work for me on Mac either. The menu function works, though.

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jul 14 2021 at 23:20):

It is working!

view this post on Zulip Ali Caglayan (Jul 14 2021 at 23:20):

Thanks @Jim Fehrle

view this post on Zulip Ali Caglayan (Jul 14 2021 at 23:20):

It's strange that the keyboard locale isn't taken into account


Last updated: Mar 28 2024 at 12:01 UTC