# HG changeset patch
# User wenzelm
# Date 1687947954 -7200
# Node ID d85d0d41b2bded4a73b1459bbe23cf79eb028c21
# Parent  2d2417a6331424f5768431ff0efe641828bebbdb
more robust;

diff -r 2d2417a63314 -r d85d0d41b2bd src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Jun 28 12:20:09 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Jun 28 12:25:54 2023 +0200
@@ -792,10 +792,10 @@
   }
 
   def read_builds(db: SQL.Database): List[Build] =
-    Data.transaction_lock(db) { Data.read_builds(db) }
+    Data.transaction_lock(db, create = true) { Data.read_builds(db) }
 
   def read_sessions(db: SQL.Database, build_uuid: String = ""): List[String] =
-    Data.transaction_lock(db) {
+    Data.transaction_lock(db, create = true) {
       Data.read_sessions_domain(db, build_uuid = build_uuid).toList.sorted
     }
 }