lib/scripts/run-polyml
2000-09-01 wenzelm 2000-09-01 GPLed; more robust handling of spaces in args / file names;
2000-08-31 wenzelm 2000-08-31 improved exit function for polyml-4.0;
2000-05-08 wenzelm 2000-05-08 always discgarb -c;
2000-03-08 wenzelm 2000-03-08 observe COMPRESS option;
1998-06-22 wenzelm 1998-06-22 check_mlhome_file;
1997-12-31 wenzelm 1997-12-31 use feeder to pipe into ML; cleaned up;
1997-12-01 wenzelm 1997-12-01 ISABELLE_TMP;
1997-07-07 wenzelm 1997-07-07 NOWRITE;
1997-04-25 wenzelm 1997-04-25 removed COPYDB flag;
1997-04-22 wenzelm 1997-04-22 removed -norc;
1997-04-11 wenzelm 1997-04-11 fixed { ... } shell syntax to accomodate bash 2.x;
1997-02-10 wenzelm 1997-02-10 tuned startup; semi fix of piping-quit peoblem (should work on systems with *real& sh);
1997-01-23 wenzelm 1997-01-23 'rm -f' instead of 'cp -f';
1996-12-16 wenzelm 1996-12-16 added symbolinput filter;
1996-12-13 wenzelm 1996-12-13 now discgarb called only for changed databases;
1996-12-09 wenzelm 1996-12-09 various fixes;
1996-12-04 wenzelm 1996-12-04 replaced cat by ucat; fixed RC handling;
1996-12-02 wenzelm 1996-12-02 run-polyml: Poly/ML startup script.