lib/scripts/unsymbolize.pl
Tue, 28 May 2002 11:06:55 +0200 paulson added <-> and ~
Mon, 11 Dec 2000 20:08:19 +0100 wenzelm harpoons;
Tue, 21 Nov 2000 19:03:27 +0100 wenzelm replace \<dots>;
Mon, 25 Sep 2000 16:31:50 +0200 wenzelm tuned replacements;
Mon, 18 Sep 2000 23:43:56 +0200 wenzelm remove unreadable symbol names from sources;
less more (0) tip