lib/scripts/run-mlworks
Fri, 09 Nov 2001 00:01:55 +0100 wenzelm got rid of obsolete input filtering;
Thu, 30 Nov 2000 20:10:29 +0100 wenzelm /usr/bin/env bash;
Thu, 28 Sep 2000 14:41:48 +0200 wenzelm added COPYDB argument;
Fri, 15 Sep 2000 20:20:45 +0200 wenzelm keep export of ISABELLE_TMP (!!!);
Fri, 15 Sep 2000 16:31:36 +0200 wenzelm unexport exports;
Tue, 05 Sep 2000 18:59:22 +0200 wenzelm fixed quotes;
Fri, 01 Sep 2000 17:54:58 +0200 wenzelm GPLed;
Wed, 31 Dec 1997 15:19:51 +0100 wenzelm use feeder to pipe into ML;
Wed, 17 Dec 1997 18:13:43 +0100 wenzelm tuned;
Tue, 16 Dec 1997 19:00:38 +0100 wenzelm MLWorks startup script (for 1.0r2 or later).
less more (0) tip