| Fri, 08 Dec 2006 23:25:54 +0100 | wenzelm | tuned use_text; | changeset | files |
| Fri, 08 Dec 2006 23:25:53 +0100 | wenzelm | added 'help' command (same of 'print_commands'); | changeset | files |
| Fri, 08 Dec 2006 23:25:52 +0100 | wenzelm | more careful evaluation of ML text, prevents spurious output; | changeset | files |