Sun, 21 Aug 2011 20:25:49 +0200 | wenzelm | avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable; | changeset | files |
Sun, 21 Aug 2011 20:04:02 +0200 | wenzelm | default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null; | changeset | files |