lib/scripts/unsymbolize.pl
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