Wed, 22 Jun 2011 16:32:36 +0200 | wenzelm | updated to jedit-4.4.1 and jedit_build-20110622; | file | diff | annotate |
Tue, 21 Jun 2011 23:08:16 +0200 | wenzelm | avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux); | file | diff | annotate |