src/Pure/System/bash.scala
changeset 73333 b70d82358c6d
parent 73273 17c28251fff0
child 73340 0ffcad1f6130
--- 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)
       }
     }
   }