Mon, 09 Aug 1999 22:22:49 +0200 tuned strings_of_context;
wenzelm [Mon, 09 Aug 1999 22:22:49 +0200] rev 7200
tuned strings_of_context; fix: check identifier;
Mon, 09 Aug 1999 22:22:01 +0200 pr / no_pr: maintain Toplevel.quiet;
wenzelm [Mon, 09 Aug 1999 22:22:01 +0200] rev 7199
pr / no_pr: maintain Toplevel.quiet;
(0) -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip