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