Mon, 27 Nov 2017 16:18:29 +0100 clarified main sessions;
wenzelm [Mon, 27 Nov 2017 16:18:29 +0100] rev 67100
clarified main sessions;
Mon, 27 Nov 2017 15:10:50 +0100 updated to official release of polyml-5.7.1;
wenzelm [Mon, 27 Nov 2017 15:10:50 +0100] rev 67099
updated to official release of polyml-5.7.1; back to more modest default heap: e.g. relevant for Pure session for ML IDE; more robust POLYML_EXE;
Mon, 27 Nov 2017 16:07:49 +0100 suppress warning;
wenzelm [Mon, 27 Nov 2017 16:07:49 +0100] rev 67098
suppress warning;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 tip