lib/scripts/symbolinput.pl
Mon, 16 Dec 1996 09:57:18 +0100 wenzelm renamed from symbol_input.pl;
less more (0) tip