# HG changeset patch
# User wenzelm
# Date 1478375087 -3600
# Node ID 2bf4fdcebd495516947e5e85f3b3db01d5fbe1a4
# Parent  73069f272f421e5a56d38070291d01b4c9051e69
more robust multithreading;

diff -r 73069f272f42 -r 2bf4fdcebd49 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Nov 05 15:07:11 2016 +0100
+++ b/src/Pure/Admin/build_history.scala	Sat Nov 05 20:44:47 2016 +0100
@@ -11,8 +11,6 @@
 import java.time.format.DateTimeFormatter
 import java.util.Locale
 
-import scala.collection.mutable
-
 
 object Build_History
 {
@@ -420,7 +418,7 @@
 
     /* Admin/build_history */
 
-    val result = new mutable.ListBuffer[(String, Bytes)]
+    var result = Synchronized(List.empty[(String, Bytes)])
 
     def progress_stdout(line: String)
     {
@@ -428,7 +426,7 @@
       val res = (log.base.implode, ssh.read_bytes(log))
       ssh.rm(log)
       progress_result(res._1, res._2)
-      result += res
+      result.change(res :: _)
     }
 
     val process_result =
@@ -439,6 +437,6 @@
         progress_stderr = progress.echo(_),
         strict = false)
 
-    (result.toList, process_result)
+    (result.value.reverse, process_result)
   }
 }