--- a/src/Pure/Tools/build_process.scala Wed Mar 01 13:23:49 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Wed Mar 01 13:30:35 2023 +0100
@@ -544,18 +544,16 @@
}
private def setup_database(): Unit =
- for (db <- _database) {
- synchronized {
- db.transaction {
- Build_Process.Data.init_database(db, build_context)
- }
+ synchronized {
+ for (db <- _database) {
+ db.transaction { Build_Process.Data.init_database(db, build_context) }
+ db.rebuild()
}
- db.rebuild()
}
private def sync_database(): Unit =
- for (db <- _database) {
- synchronized {
+ synchronized {
+ for (db <- _database) {
db.transaction {
_state =
Build_Process.Data.update_database(
@@ -564,7 +562,8 @@
}
}
- def close(): Unit = _database.foreach(_.close())
+ def close(): Unit =
+ synchronized { _database.foreach(_.close()) }
/* policy operations */