Wed, 05 Nov 1997 11:49:34 +0100 | wenzelm | adapted typed_print_translation; | changeset | files |
Wed, 05 Nov 1997 11:49:07 +0100 | wenzelm | tuned record_info; | changeset | files |
Wed, 05 Nov 1997 11:45:51 +0100 | wenzelm | fixed exception OPTION; | changeset | files |