"Giglio, James" wrote:
> How about an addition to global options that allows the user to change font size and characteristics of the main menu and the drop-downs? Some of us are old guys, and need to make these fonts larger and/or darker.
Someone should write a plugin that loads values from jEdit properties and
puts them in the Swing UIDefaults plugin.