| Tue, 11 Sep 2012 13:06:13 +0200 | blanchet | reverted "id" change: The problem is rather that the "%c. f c" argument sometimes gets eta-reduced | changeset | files |
| Tue, 11 Sep 2012 16:10:54 +0200 | wenzelm | replaced jedit_relative_font_size by jedit_font_scale; | changeset | files |
| Tue, 11 Sep 2012 15:59:35 +0200 | wenzelm | need to provide label via some jEdit property; | changeset | files |
| Tue, 11 Sep 2012 15:47:42 +0200 | wenzelm | some support to organize options in sections; | changeset | files |