src/Pure/System/bash.scala
changeset 73265 76c9fcf80f96
parent 73263 ad60214bef09
child 73268 c8abfe393c16
equal deleted inserted replaced
73264:440546ea20e6 73265:76c9fcf80f96
   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   }