# HG changeset patch
# User wenzelm
# Date 1691692768 -7200
# Node ID f5fb5bb2533fdf96b136a2aa508e30d4608fd888
# Parent  8f45302a9ff07ad4e042cbfdf02470764ff0fea8
clarified option name (see also ff43a524aa5d);

diff -r 8f45302a9ff0 -r f5fb5bb2533f etc/options
--- a/etc/options	Thu Aug 10 20:30:37 2023 +0200
+++ b/etc/options	Thu Aug 10 20:39:28 2023 +0200
@@ -195,7 +195,7 @@
 option build_engine : string = ""
   -- "alternative session build engine"
 
-option build_database_test : bool = false
+option build_database : bool = false
   -- "expose state of build process via central database"
 
 option build_database_slice : real = 300
diff -r 8f45302a9ff0 -r f5fb5bb2533f src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Thu Aug 10 20:30:37 2023 +0200
+++ b/src/Pure/Thy/store.scala	Thu Aug 10 20:39:28 2023 +0200
@@ -294,7 +294,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 build_database: Boolean = options.bool("build_database")
 
   def open_server(): SSH.Server =
     PostgreSQL.open_server(options,
@@ -327,7 +327,7 @@
     path: Path = Path.explode("$ISABELLE_HOME_USER/build.db"),
     server: SSH.Server = SSH.no_server
   ): Option[SQL.Database] = {
-    if (build_database_test) Some(open_build_database(path, server = server)) else None
+    if (build_database) Some(open_build_database(path, server = server)) else None
   }
 
   def try_open_database(
diff -r 8f45302a9ff0 -r f5fb5bb2533f src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Aug 10 20:30:37 2023 +0200
+++ b/src/Pure/Tools/build.scala	Thu Aug 10 20:39:28 2023 +0200
@@ -111,7 +111,7 @@
     def build_options(options: Options, build_hosts: List[Build_Cluster.Host] = Nil): Options = {
       val options1 = options + "completion_limit=0" + "editor_tracing_messages=0"
       if (build_hosts.isEmpty) options1
-      else options1 + "build_database_server" + "build_database_test"
+      else options1 + "build_database_server" + "build_database"
     }
 
     def process_options(options: Options, node_info: Host.Node_Info): Options =
@@ -581,7 +581,7 @@
       var max_jobs = 1
       var options =
         Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS :::
-          List(Options.Spec.make("build_database_test")))
+          List(Options.Spec.make("build_database")))
       var verbose = false
 
       val getopts = Getopts("""