diff -r 4dabf4db7cec -r b7072c97e0ca src/Pure/Build/build_job.scala --- a/src/Pure/Build/build_job.scala Wed Oct 08 10:49:18 2025 +0200 +++ b/src/Pure/Build/build_job.scala Wed Oct 08 11:03:18 2025 +0200 @@ -357,7 +357,8 @@ } session.runtime_statistics += Session.Consumer("ML_statistics") { - case Session.Runtime_Statistics(props) => runtime_statistics += props + case Session.Runtime_Statistics(props) => + session.synchronized { runtime_statistics += props } } session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") {