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