| Mon, 24 Aug 2009 08:33:40 +0200 | boehmes | do not introduce additional newlines | changeset | files |
| Sat, 22 Aug 2009 23:22:17 +0200 | wenzelm | tuned; | changeset | files |
| Sat, 22 Aug 2009 23:20:36 +0200 | wenzelm | generalized settings; | changeset | files |
| Sat, 22 Aug 2009 23:16:11 +0200 | wenzelm | removed jedit setup -- now a self-contained component (external); | changeset | files |