Wed, 22 Oct 2008 14:15:46 +0200 | haftmann | tuned | changeset | files |
Wed, 22 Oct 2008 14:15:45 +0200 | haftmann | code identifier namings are no longer imperative | changeset | files |
Wed, 22 Oct 2008 14:15:44 +0200 | haftmann | tuned typedef interface | changeset | files |
Wed, 22 Oct 2008 14:15:43 +0200 | haftmann | slightly tuned | changeset | files |
Wed, 22 Oct 2008 14:15:42 +0200 | haftmann | fixed | changeset | files |
Tue, 21 Oct 2008 23:54:42 +0200 | wenzelm | less ambitious default for JEDIT_JAVA_OPTIONS; | changeset | files |
Tue, 21 Oct 2008 22:21:28 +0200 | wenzelm | JEDIT_OPTIONS: moved -settings to interface script (more robust); | changeset | files |