Mon, 29 Nov 1993 12:28:09 +0100 improved comments;
wenzelm [Mon, 29 Nov 1993 12:28:09 +0100] rev 165
improved comments;
Mon, 29 Nov 1993 12:27:29 +0100 added SCANNER;
wenzelm [Mon, 29 Nov 1993 12:27:29 +0100] rev 164
added SCANNER; changed scan_any: no longer uses take_prefix;
(0) -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip