Fri, 19 Dec 2008 23:56:58 +0100 | wenzelm | disabled tracing; | changeset | files |
Fri, 19 Dec 2008 23:55:07 +0100 | wenzelm | misc tuning; | changeset | files |
Fri, 19 Dec 2008 23:54:24 +0100 | wenzelm | proper spelling of JEDIT_JAVA_OPTIONS; | changeset | files |