| Sun, 28 Dec 2008 23:20:57 +0100 | wenzelm | disabled old jedit plugin; | changeset | files |
| Sun, 28 Dec 2008 20:25:39 +0100 | wenzelm | more markup elements; | changeset | files |
| Sun, 28 Dec 2008 16:39:27 +0100 | wenzelm | more markup elements; | changeset | files |
| Sat, 27 Dec 2008 17:49:15 +0100 | krauss | removed duplicate sum_case used only by function package; | changeset | files |