clarified lines (again);
authorwenzelm
Sun, 21 Feb 2021 00:49:09 +0100
changeset 73265 76c9fcf80f96
parent 73264 440546ea20e6
child 73266 d6a664daa285
clarified lines (again);
src/Pure/ROOT.ML
src/Pure/System/bash.scala
--- 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"
+
--- 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))