| Wed, 06 Jul 1994 12:49:56 +0200 | wenzelm | various minor changes (names and comments); | changeset | files |
| Wed, 06 Jul 1994 11:53:30 +0200 | clasohm | changed comment for const_name | changeset | files |
| Wed, 06 Jul 1994 11:36:00 +0200 | wenzelm | changed comment only; | changeset | files |