Mon, 16 Dec 1996 09:57:34 +0100 | wenzelm | renamed to symbolinput.pl; | changeset | files |
Mon, 16 Dec 1996 09:57:18 +0100 | wenzelm | renamed from symbol_input.pl; | changeset | files |
Mon, 16 Dec 1996 09:56:28 +0100 | wenzelm | minor tuning; | changeset | files |
Mon, 16 Dec 1996 09:53:30 +0100 | wenzelm | now fails if getsettings not found; | changeset | files |
Fri, 13 Dec 1996 18:45:58 +0100 | oheimb | adaptions for symbol font | changeset | files |
Fri, 13 Dec 1996 18:40:50 +0100 | oheimb | adaptions for symbol font | changeset | files |