equal
deleted
inserted
replaced
85 |
85 |
86 |
86 |
87 |
87 |
88 (*** ML command execution ***) |
88 (*** ML command execution ***) |
89 |
89 |
|
90 |
|
91 (*For version 109.21 and later: |
|
92 val use_string = Compiler.Interact.useStream o TextIO.openString o implode; |
|
93 *) |
|
94 |
|
95 (*For versions prior to 109.21:*) |
90 fun use_string commands = |
96 fun use_string commands = |
91 Compiler.Interact.use_stream (open_string (implode commands)); |
97 Compiler.Interact.use_stream (open_string (implode commands)); |
92 |
|
93 (*For later versions of Standard ML of New Jersey use... |
|
94 val use_string = Compiler.Interact.useStream o TextIO.openString o implode; |
|
95 *) |
|
96 |
98 |
97 (*** System command execution ***) |
99 (*** System command execution ***) |
98 |
100 |
99 (*Execute an Unix command which doesn't take any input from stdin and |
101 (*Execute an Unix command which doesn't take any input from stdin and |
100 sends its output to stdout. |
102 sends its output to stdout. |