boehmes [Mon, 10 Jan 2011 17:39:54 +0100] rev 41497
dropped superfluous error message
krauss [Mon, 10 Jan 2011 17:37:11 +0100] rev 41496
removed obsolete make target (now in doc-src, cf. 28b487cd9e15)
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