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: Nov 07 2025 at 16:23 UTC