Tue, 20 Oct 1998 16:25:54 +0200 | wenzelm | quiet_mode, message; | changeset | files |
Tue, 20 Oct 1998 16:25:14 +0200 | wenzelm | structure Hidden = struct end; | changeset | files |
Tue, 20 Oct 1998 16:24:45 +0200 | wenzelm | hiding private stuff; | changeset | files |