Thu, 28 May 1998 12:24:05 +0200 wenzelm tuned header;
Thu, 28 May 1998 12:23:11 +0200 wenzelm version under control of Admin/makedist;
Thu, 28 May 1998 12:22:37 +0200 wenzelm README, Pure/ROOT.ML: version set automatically;
Thu, 28 May 1998 12:22:05 +0200 wenzelm version under control of Admin/makedist;
(0) -3000 -1000 -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip