lib/Tools/symbolinput
1997-04-22 wenzelm 1997-04-22 removed -norc;
1997-02-06 wenzelm 1997-02-06 now falls back on ucat instead of cat;
1996-12-16 wenzelm 1996-12-16 symbolinput - translate symbols into \<...> sequences;