lib/scripts/run-polyml-5.0
Tue, 06 Feb 2007 18:02:28 +0100 wenzelm cc: removed option -lstdc++, which seems to be unnecessry, but causes problems on some platforms;
Sun, 10 Dec 2006 15:30:33 +0100 wenzelm hardwired option -q;
Fri, 08 Dec 2006 23:25:52 +0100 wenzelm more careful evaluation of ML text, prevents spurious output;
Fri, 08 Dec 2006 22:17:20 +0100 wenzelm root function: restore default interrupt handler;
Tue, 05 Dec 2006 18:33:29 +0100 wenzelm setup for polyml-5.0;
less more (0) tip