author | wenzelm |
Sat, 15 Jul 2023 20:34:06 +0200 | |
changeset 78350 | db76217fe9b6 |
parent 78349 | a9b544b6fc60 |
child 78351 | 9f2cfb9873bb |
--- a/src/Pure/Tools/build_process.scala Sat Jul 15 20:08:19 2023 +0200 +++ b/src/Pure/Tools/build_process.scala Sat Jul 15 20:34:06 2023 +0200 @@ -907,8 +907,8 @@ _build_database match { case None => body case Some(db) => + progress.asInstanceOf[Database_Progress].sync() Build_Process.Data.transaction_lock(db) { - progress.asInstanceOf[Database_Progress].sync() _state = Build_Process.Data.pull_database(db, worker_uuid, hostname, _state) val res = body _state =