lib/scripts/run-polyml
Fri, 11 Apr 1997 17:30:15 +0200 wenzelm fixed { ... } shell syntax to accomodate bash 2.x;
Mon, 10 Feb 1997 16:16:55 +0100 wenzelm tuned startup;
Thu, 23 Jan 1997 18:10:29 +0100 wenzelm 'rm -f' instead of 'cp -f';
Mon, 16 Dec 1996 09:59:18 +0100 wenzelm added symbolinput filter;
Fri, 13 Dec 1996 17:48:03 +0100 wenzelm now discgarb called only for changed databases;
Mon, 09 Dec 1996 16:42:24 +0100 wenzelm various fixes;
Wed, 04 Dec 1996 13:18:26 +0100 wenzelm replaced cat by ucat;
Mon, 02 Dec 1996 18:24:01 +0100 wenzelm run-polyml: Poly/ML startup script.
less more (0) tip