| Sat, 19 Jul 2008 11:05:18 +0200 | wenzelm | build jedit plugin only if jedit is available; | changeset | files |
| Fri, 18 Jul 2008 22:03:20 +0200 | wenzelm | misc tuning; | changeset | files |
| Fri, 18 Jul 2008 18:25:57 +0200 | haftmann | more class instantiations | changeset | files |