--- a/src/Pure/Tools/build.scala Wed Jun 28 12:16:02 2023 +0200
+++ b/src/Pure/Tools/build.scala Wed Jun 28 12:20:09 2023 +0200
@@ -382,11 +382,11 @@
/* identified builds */
def read_builds(options: Options): List[Build_Process.Build] =
- using_option(Store(options).maybe_open_build_database(Build_Process.Data.database))(
+ using_option(Store(options).maybe_open_build_database())(
Build_Process.read_builds).getOrElse(Nil).filter(_.active)
def print_builds(options: Options, builds: List[Build_Process.Build]): String =
- using_optional(Store(options).maybe_open_build_database(Build_Process.Data.database)) { build_database =>
+ using_optional(Store(options).maybe_open_build_database()) { build_database =>
val print_database =
build_database match {
case None => ""
@@ -433,7 +433,7 @@
val build_options = store.options
val sessions =
- using_optional(store.maybe_open_build_database(Build_Process.Data.database)) {
+ using_optional(store.maybe_open_build_database()) {
case None => error("Cannot access build database")
case Some(db) => Build_Process.read_sessions(db, build_master.build_uuid)
}