Menu
▾
▴
[ jEdit-devel ] button, menu items, font size.
|
From: Eric B. <el...@gm...> - 2017-01-17 22:41:32
|
Is there a way to set them, these settings are grey-ed out and I'm unable to change them. -- Learn from the past. Live in the present. Work towards the future. Blog: http://eric-berry.blogspot.com jEdit <http://www.jedit.org> - Programmer's Text Editor |