| Fri, 12 Oct 2012 23:38:48 +0200 | wenzelm | further refinement of jEdit line range, avoiding lack of final \n; | changeset | files |
| Fri, 12 Oct 2012 22:53:20 +0200 | wenzelm | more uniform tooltip color; | changeset | files |
| Fri, 12 Oct 2012 22:10:45 +0200 | wenzelm | more NEWS; | changeset | files |