Mon, 10 Jan 2011 18:58:54 +0100 be more precise: also merge option values
boehmes [Mon, 10 Jan 2011 18:58:54 +0100] rev 41499
be more precise: also merge option values
Mon, 10 Jan 2011 17:41:45 +0100 only print warning in a visible context (previously, the warning was printed more than once)
boehmes [Mon, 10 Jan 2011 17:41:45 +0100] rev 41498
only print warning in a visible context (previously, the warning was printed more than once)
Mon, 10 Jan 2011 17:39:54 +0100 dropped superfluous error message
boehmes [Mon, 10 Jan 2011 17:39:54 +0100] rev 41497
dropped superfluous error message
Mon, 10 Jan 2011 17:37:11 +0100 removed obsolete make target (now in doc-src, cf. 28b487cd9e15)
krauss [Mon, 10 Jan 2011 17:37:11 +0100] rev 41496
removed obsolete make target (now in doc-src, cf. 28b487cd9e15)
Mon, 10 Jan 2011 17:22:48 +0100 updated for polyml-5.4.0;
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;
Mon, 10 Jan 2011 16:56:47 +0100 made SML/NJ happy;
wenzelm [Mon, 10 Jan 2011 16:56:47 +0100] rev 41494
made SML/NJ happy;
Mon, 10 Jan 2011 16:45:28 +0100 added merge_options convenience;
wenzelm [Mon, 10 Jan 2011 16:45:28 +0100] rev 41493
added merge_options convenience;
Mon, 10 Jan 2011 16:07:16 +0100 tuned string_of_int to avoid allocation for small integers;
wenzelm [Mon, 10 Jan 2011 16:07:16 +0100] rev 41492
tuned string_of_int to avoid allocation for small integers;
Mon, 10 Jan 2011 15:45:46 +0100 eliminated Int.toString;
wenzelm [Mon, 10 Jan 2011 15:45:46 +0100] rev 41491
eliminated Int.toString;
Mon, 10 Jan 2011 15:30:17 +0100 eliminated obsolete LargeInt -- Int is unbounded;
wenzelm [Mon, 10 Jan 2011 15:30:17 +0100] rev 41490
eliminated obsolete LargeInt -- Int is unbounded;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip