Thu, 07 Dec 2006 17:58:48 +0100 tuned pretty_src output;
wenzelm [Thu, 07 Dec 2006 17:58:48 +0100] rev 21697
tuned pretty_src output;
Thu, 07 Dec 2006 17:58:46 +0100 simplified add_abbrevs: no mixfix;
wenzelm [Thu, 07 Dec 2006 17:58:46 +0100] rev 21696
simplified add_abbrevs: no mixfix;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip