tuned;
authorwenzelm
Wed, 28 Jun 2023 11:44:09 +0200
changeset 78220 82efaf1bf3c7
parent 78219 af2963b74752
child 78221 60fa7a0b9372
tuned;
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)
       }