--- a/src/Pure/System/bash.ML Sun Feb 07 17:00:03 2021 +0100
+++ b/src/Pure/System/bash.ML Sun Feb 07 20:39:15 2021 +0100
@@ -191,12 +191,12 @@
let open XML.Decode in
variant
[fn ([], []) => raise Exn.Interrupt,
- fn ([a], []) => error a,
+ fn ([], a) => error (YXML.string_of_body a),
fn ([a, b], c) =>
let
val rc = int_atom a;
val pid = int_atom b;
- val (out, err) = pair string string c;
+ val (out, err) = pair I I c |> apply2 YXML.string_of_body;
in {out = out, err = err, rc = rc, terminate = fn () => terminate (SOME pid)} end]
end;
--- a/src/Pure/System/bash.scala Sun Feb 07 17:00:03 2021 +0100
+++ b/src/Pure/System/bash.scala Sun Feb 07 20:39:15 2021 +0100
@@ -230,7 +230,7 @@
val string = XML.Encode.string
variant(List(
{ case _ if is_interrupt => (Nil, Nil) },
- { case Exn.Exn(exn) => (List(Exn.message(exn)), Nil) },
+ { case Exn.Exn(exn) => (Nil, string(Exn.message(exn))) },
{ case Exn.Res((res, pid)) =>
val out = Library.terminate_lines(res.out_lines)
val err = Library.terminate_lines(res.err_lines)