Sun, 03 Dec 2017 19:00:55 +0100 | wenzelm | tuned; | changeset | files |
Sun, 03 Dec 2017 18:53:49 +0100 | wenzelm | misc tuning and modernization; | changeset | files |
Sun, 03 Dec 2017 13:22:09 +0100 | wenzelm | discontinued old 'def' command; | changeset | files |