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