equal
deleted
inserted
replaced
106 OS.FileSys.remove tmpName; |
106 OS.FileSys.remove tmpName; |
107 result |
107 result |
108 end; |
108 end; |
109 |
109 |
110 |
110 |
111 (*Don't know what the boolean is for*) |
111 (*"false" writes an image file that is executed via the MLWorks "mlimage" |
|
112 script, while "true" would yield a larger, self-contained executable.*) |
112 fun xML filename = Shell.saveImage (filename, false); |
113 fun xML filename = Shell.saveImage (filename, false); |
113 |
114 |
114 |
115 |
115 (*Non-printing and 8-bit chars are forbidden in string constants*) |
116 (*Non-printing and 8-bit chars are forbidden in string constants*) |
116 val needs_filtered_use = true; |
117 val needs_filtered_use = true; |