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