Mon, 17 May 1999 21:35:18 +0200 | wenzelm | tuned; | changeset | files |
Mon, 17 May 1999 21:34:45 +0200 | wenzelm | cleaned comments; | changeset | files |
Mon, 17 May 1999 21:33:22 +0200 | wenzelm | ThyInfo.finalize_all renamed to ThyInfo.finish; | changeset | files |