Corrected a comment
authorpaulson
Tue Aug 05 10:50:24 1997 +0200 (1997-08-05)
changeset 358700ea30ea0734
parent 3586 2ee1ed79c802
child 3588 e487bf0ed6c4
Corrected a comment
src/Pure/ML-Systems/MLWorks.ML
     1.1 --- a/src/Pure/ML-Systems/MLWorks.ML	Mon Aug 04 11:50:35 1997 +0200
     1.2 +++ b/src/Pure/ML-Systems/MLWorks.ML	Tue Aug 05 10:50:24 1997 +0200
     1.3 @@ -108,7 +108,8 @@
     1.4    end;
     1.5  
     1.6  
     1.7 -(*Don't know what the boolean is for*)
     1.8 +(*"false" writes an image file that is executed via the MLWorks "mlimage" 
     1.9 +  script, while "true" would yield a larger, self-contained executable.*)
    1.10  fun xML filename = Shell.saveImage (filename, false);
    1.11  
    1.12