--- 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)
}
}
}