| changeset 26213 | 3a190cb91c6c |
| parent 25124 | a7dd8d3bf969 |
| child 26375 | 234f10289d97 |
--- 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