# HG changeset patch
# User wenzelm
# Date 1687945449 -7200
# Node ID 82efaf1bf3c75845948bf3e4da139240171992d6
# Parent  af2963b7475262a10d513c2762e489120d6240dc
tuned;

diff -r af2963b74752 -r 82efaf1bf3c7 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Jun 28 11:35:02 2023 +0200
+++ b/src/Pure/Tools/build.scala	Wed Jun 28 11:44:09 2023 +0200
@@ -418,7 +418,7 @@
     val build_options = store.options
 
     val sessions =
-      using_optional(Store(options).maybe_open_build_database(Build_Process.Data.database)) {
+      using_optional(store.maybe_open_build_database(Build_Process.Data.database)) {
         case None => error("Cannot access build database")
         case Some(db) => Build_Process.read_sessions(db, build_master.build_uuid)
       }