author | wenzelm |
Thu, 06 Mar 2008 19:21:24 +0100 (2008-03-06) | |
changeset 26213 | 3a190cb91c6c |
parent 26212 | 225b40bf36a7 |
child 26214 | 73ed8cb8ac4d |
--- a/lib/scripts/run-polyml-5.0 Thu Mar 06 19:21:23 2008 +0100 +++ b/lib/scripts/run-polyml-5.0 Thu Mar 06 19:21:24 2008 +0100 @@ -3,7 +3,7 @@ # $Id$ # Author: Makarius # -# Poly/ML startup script (for 5.0) +# Poly/ML 5.0 startup script. export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE