Stream: General

Topic: jEdit font size, Macbook


view this post on Zulip Peter Koepke (Oct 11 2025 at 22:00):

Are there key combinations for increasing/decreasing jEdit font size on a recent MacBook Air?

view this post on Zulip Yosuke Ito (Oct 12 2025 at 00:05):

Doesn't Command + minus/plus work?
Maybe you want register your own keybind through
Isabelle > Settings > Global Options > Shortcuts.


Last updated: Oct 18 2025 at 16:23 UTC