--- 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
--- 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(
--- 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("""