# HG changeset patch
# User wenzelm
# Date 1613864949 -3600
# Node ID 76c9fcf80f960756e68a8375a70b7b0fba6bd1b5
# Parent  440546ea20e61f784461b59e62fbe047abee5415
clarified lines (again);

diff -r 440546ea20e6 -r 76c9fcf80f96 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Feb 20 23:01:35 2021 +0100
+++ b/src/Pure/ROOT.ML	Sun Feb 21 00:49:09 2021 +0100
@@ -354,3 +354,4 @@
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML"
+
diff -r 440546ea20e6 -r 76c9fcf80f96 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sat Feb 20 23:01:35 2021 +0100
+++ b/src/Pure/System/bash.scala	Sun Feb 21 00:49:09 2021 +0100
@@ -227,8 +227,8 @@
           { case _ if is_interrupt => (Nil, Nil) },
           { case Exn.Exn(exn) => (Nil, string(Exn.message(exn))) },
           { case Exn.Res(res) =>
-              val out = Library.terminate_lines(res.out_lines)
-              val err = Library.terminate_lines(res.err_lines)
+              val out = if (res.out_lines.isEmpty) "" else Library.terminate_lines(res.out_lines)
+              val err = if (res.err_lines.isEmpty) "" else Library.terminate_lines(res.err_lines)
               (List(int_atom(res.rc)), pair(string, string)(out, err)) }))
       }
       YXML.string_of_body(encode(result))