src/Tools/jEdit/src/jedit_options.scala
Sat, 18 May 2013 12:41:31 +0200 wenzelm explicit notion of public options, which are shown in the editor options dialog;
less more (0) -10 -1 tip