src/Pure/ML-Systems/MLWorks.ML
changeset 3587 00ea30ea0734
parent 3539 d4443afc8d28
child 3597 3ac6d6bcae42
     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