| Mon, 09 Mar 1998 16:15:24 +0100 | wenzelm | replaced $LOGNAME by $USER; | changeset | files |
| Mon, 09 Mar 1998 16:14:46 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 09 Mar 1998 16:14:32 +0100 | wenzelm | Symbol.is_*; | changeset | files |
| Mon, 09 Mar 1998 16:14:15 +0100 | wenzelm | adapted to new scanner, baroque chars; | changeset | files |