# HG changeset patch
# User wenzelm
# Date 1594477945 -7200
# Node ID 5469bacf5573294e41cfec6a7d2899b6669eaff7
# Parent  6c6609fd898c5f16c8d4cdc3e0cdb0ee49eb408c
avoid duplicate Timing messages (see also 5c4800f6b25a);

diff -r 6c6609fd898c -r 5469bacf5573 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Jul 11 16:25:17 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jul 11 16:32:25 2020 +0200
@@ -238,7 +238,6 @@
           }
 
           val stdout = new StringBuilder(1000)
-          val stderr = new StringBuilder(1000)
           val messages = new mutable.ListBuffer[XML.Elem]
           val command_timings = new mutable.ListBuffer[Properties.T]
           val theory_timings = new mutable.ListBuffer[Properties.T]
@@ -320,9 +319,6 @@
                 if (msg.is_stdout) {
                   stdout ++= Symbol.encode(XML.content(message))
                 }
-                else if (msg.is_stderr) {
-                  stderr ++= Symbol.encode(XML.content(message))
-                }
                 else if (Protocol.is_exported(message)) {
                   messages += message
                 }
@@ -368,8 +364,7 @@
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply)
 
-          val result =
-            process_result.output(process_output).error(Library.trim_line(stderr.toString))
+          val result = process_result.output(process_output)
 
           errors match {
             case Exn.Res(Nil) => result