wenzelm [Mon, 10 Jan 2011 17:22:48 +0100] rev 41495
updated for polyml-5.4.0;
discontinued old-fashioned POLY_HOME via path;
more robust handling of polyml-version, preferably provided by Poly/ML distribution itself;
wenzelm [Mon, 10 Jan 2011 16:56:47 +0100] rev 41494
made SML/NJ happy;
wenzelm [Mon, 10 Jan 2011 16:45:28 +0100] rev 41493
added merge_options convenience;
wenzelm [Mon, 10 Jan 2011 16:07:16 +0100] rev 41492
tuned string_of_int to avoid allocation for small integers;
wenzelm [Mon, 10 Jan 2011 15:45:46 +0100] rev 41491
eliminated Int.toString;
wenzelm [Mon, 10 Jan 2011 15:30:17 +0100] rev 41490
eliminated obsolete LargeInt -- Int is unbounded;
wenzelm [Mon, 10 Jan 2011 15:19:48 +0100] rev 41489
standardized split_last/last_elem towards List.last;
eliminated obsolete Library.last_elem;
bulwahn [Mon, 10 Jan 2011 08:18:49 +0100] rev 41488
removing dead code; tuned
bulwahn [Mon, 10 Jan 2011 08:18:48 +0100] rev 41487
made SML/NJ happy
wenzelm [Sun, 09 Jan 2011 21:33:41 +0100] rev 41486
reverted 08240feb69c7 -- breaks positions of reports;