# HG changeset patch
# User wenzelm
# Date 1686857077 -7200
# Node ID d47b2a04fc04640c5f5bf39bc9b3edeca75ebb29
# Parent  5454bec8f5c67814f8bb7c1bb78161220083c68b
tuned signature;

diff -r 5454bec8f5c6 -r d47b2a04fc04 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Jun 15 17:29:29 2023 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Jun 15 21:24:37 2023 +0200
@@ -1496,6 +1496,7 @@
       input_dirs.map(_ + database(name)).find(_.is_file)
 
     def build_database_server: Boolean = options.bool("build_database_server")
+    def build_database_test: Boolean = options.bool("build_database_test")
 
     def open_database_server(): PostgreSQL.Database =
       PostgreSQL.open_database(
@@ -1515,7 +1516,7 @@
     val build_database: Path = Path.explode("$ISABELLE_HOME_USER/build.db")
 
     def open_build_database(): Option[SQL.Database] =
-      if (!options.bool("build_database_test")) None
+      if (!build_database_test) None
       else if (build_database_server) Some(open_database_server())
       else Some(SQLite.open_database(build_database, restrict = true))