equal
deleted
inserted
replaced
3 |
3 |
4 Generic GNU bash processes (no provisions to propagate interrupts, but |
4 Generic GNU bash processes (no provisions to propagate interrupts, but |
5 could work via the controlling tty). |
5 could work via the controlling tty). |
6 *) |
6 *) |
7 |
7 |
8 structure Bash = |
8 signature BASH = |
|
9 sig |
|
10 val process: string -> {output: string, rc: int, terminate: unit -> unit} |
|
11 end; |
|
12 |
|
13 structure Bash: BASH = |
9 struct |
14 struct |
10 |
15 |
11 fun process script = |
16 fun process script = |
12 let |
17 let |
13 val id = serial_string (); |
18 val id = serial_string (); |