equal
deleted
inserted
replaced
17 val cwd: Path.T -> params -> params |
17 val cwd: Path.T -> params -> params |
18 val putenv: (string * string) list -> params -> params |
18 val putenv: (string * string) list -> params -> params |
19 val redirect: params -> params |
19 val redirect: params -> params |
20 val timeout: Time.time -> params -> params |
20 val timeout: Time.time -> params -> params |
21 val description: string -> params -> params |
21 val description: string -> params -> params |
|
22 val server_run: string |
|
23 val server_kill: string |
|
24 val server_uuid: string |
|
25 val server_interrupt: string |
|
26 val server_failure: string |
|
27 val server_result: string |
22 end; |
28 end; |
23 |
29 |
24 structure Bash: BASH = |
30 structure Bash: BASH = |
25 struct |
31 struct |
26 |
32 |
89 map_params (fn (script, input, cwd, putenv, redirect, timeout, _) => |
95 map_params (fn (script, input, cwd, putenv, redirect, timeout, _) => |
90 (script, input, cwd, putenv, redirect, timeout, description)); |
96 (script, input, cwd, putenv, redirect, timeout, description)); |
91 |
97 |
92 end; |
98 end; |
93 |
99 |
|
100 |
|
101 (* server messages *) |
|
102 |
|
103 val server_run = "run"; |
|
104 val server_kill = "kill"; |
|
105 |
|
106 val server_uuid = "uuid"; |
|
107 val server_interrupt = "interrupt"; |
|
108 val server_failure = "failure"; |
|
109 val server_result = "result"; |
|
110 |
94 end; |
111 end; |