| Fri, 02 Dec 2011 14:26:43 +0100 | wenzelm | eliminated some legacy operations; | changeset | files |
| Fri, 02 Dec 2011 13:59:25 +0100 | wenzelm | removed dead code, which has never been active in recorded history; | changeset | files |
| Fri, 02 Dec 2011 13:51:36 +0100 | wenzelm | do not open ML structures; | changeset | files |