Tue, 04 Nov 1997 16:57:52 +0100 tuned to make non-Poly/MLs happy;
wenzelm [Tue, 04 Nov 1997 16:57:52 +0100] rev 4128
tuned to make non-Poly/MLs happy;
Tue, 04 Nov 1997 16:49:35 +0100 tuned 'records' stuff;
wenzelm [Tue, 04 Nov 1997 16:49:35 +0100] rev 4127
tuned 'records' stuff;
Tue, 04 Nov 1997 16:46:02 +0100 added pretty_ctyp;
wenzelm [Tue, 04 Nov 1997 16:46:02 +0100] rev 4126
added pretty_ctyp;
(0) -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip