equal
deleted
inserted
replaced
225 val string = XML.Encode.string |
225 val string = XML.Encode.string |
226 variant(List( |
226 variant(List( |
227 { case _ if is_interrupt => (Nil, Nil) }, |
227 { case _ if is_interrupt => (Nil, Nil) }, |
228 { case Exn.Exn(exn) => (Nil, string(Exn.message(exn))) }, |
228 { case Exn.Exn(exn) => (Nil, string(Exn.message(exn))) }, |
229 { case Exn.Res(res) => |
229 { case Exn.Res(res) => |
230 val out = Library.terminate_lines(res.out_lines) |
230 val out = if (res.out_lines.isEmpty) "" else Library.terminate_lines(res.out_lines) |
231 val err = Library.terminate_lines(res.err_lines) |
231 val err = if (res.err_lines.isEmpty) "" else Library.terminate_lines(res.err_lines) |
232 (List(int_atom(res.rc)), pair(string, string)(out, err)) })) |
232 (List(int_atom(res.rc)), pair(string, string)(out, err)) })) |
233 } |
233 } |
234 YXML.string_of_body(encode(result)) |
234 YXML.string_of_body(encode(result)) |
235 } |
235 } |
236 } |
236 } |