diff -r 91703452523d -r b70d82358c6d src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Mon Mar 01 17:44:44 2021 +0100 +++ b/src/Pure/System/bash.scala Mon Mar 01 18:11:06 2021 +0100 @@ -223,11 +223,12 @@ case _ if is_interrupt => "" case Exn.Exn(exn) => Exn.message(exn) case Exn.Res(res) => - (res.rc.toString :: - res.timing.elapsed.ms.toString :: - res.timing.cpu.ms.toString :: - res.out_lines.length.toString :: - res.out_lines ::: res.err_lines).mkString("\u0000") + Library.cat_strings0( + res.rc.toString :: + res.timing.elapsed.ms.toString :: + res.timing.cpu.ms.toString :: + res.out_lines.length.toString :: + res.out_lines ::: res.err_lines) } } }