# HG changeset patch
# User wenzelm
# Date 1689446046 -7200
# Node ID db76217fe9b65004ae202ceacffba6aae732cb18
# Parent  a9b544b6fc60a34c035a862a1ed5731716e272d9
more robust: avoid nested transactions (on disjoint tables);

diff -r a9b544b6fc60 -r db76217fe9b6 src/Pure/Tools/build_process.scala
--- 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 =