# HG changeset patch
# User paulson
# Date 870771024 -7200
# Node ID 00ea30ea0734d1f6e3358483474577d30df97e0b
# Parent  2ee1ed79c802c3535c0b8b5ce1c4e4894c479630
Corrected a comment

diff -r 2ee1ed79c802 -r 00ea30ea0734 src/Pure/ML-Systems/MLWorks.ML
--- a/src/Pure/ML-Systems/MLWorks.ML	Mon Aug 04 11:50:35 1997 +0200
+++ b/src/Pure/ML-Systems/MLWorks.ML	Tue Aug 05 10:50:24 1997 +0200
@@ -108,7 +108,8 @@
   end;
 
 
-(*Don't know what the boolean is for*)
+(*"false" writes an image file that is executed via the MLWorks "mlimage" 
+  script, while "true" would yield a larger, self-contained executable.*)
 fun xML filename = Shell.saveImage (filename, false);