# HG changeset patch
# User wenzelm
# Date 1204827684 -3600
# Node ID 3a190cb91c6cd869d671b98b2b8176f0e2d5a85e
# Parent  225b40bf36a7eb4b708b2bfdb739fa360a73db4c
tuned comment;

diff -r 225b40bf36a7 -r 3a190cb91c6c lib/scripts/run-polyml-5.0
--- 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