lib/Tools/symbolinput
Tue, 22 Apr 1997 11:37:12 +0200 wenzelm removed -norc;
Thu, 06 Feb 1997 18:22:59 +0100 wenzelm now falls back on ucat instead of cat;
Mon, 16 Dec 1996 09:58:16 +0100 wenzelm symbolinput - translate symbols into \<...> sequences;
less more (0) tip