Thu, 16 Oct 1997 14:52:35 +0200 tuned;
wenzelm [Thu, 16 Oct 1997 14:52:35 +0200] rev 3901
tuned;
Thu, 16 Oct 1997 14:48:10 +0200 removed begin;
wenzelm [Thu, 16 Oct 1997 14:48:10 +0200] rev 3900
removed begin; added global section; added global_names flag (tmp), default true;
Thu, 16 Oct 1997 14:46:55 +0200 fixed prep_ext;
wenzelm [Thu, 16 Oct 1997 14:46:55 +0200] rev 3899
fixed prep_ext;
(0) -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip