--- a/src/Pure/Build/build_schedule.scala Thu Feb 15 12:18:25 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Thu Feb 15 12:37:52 2024 +0100
@@ -1038,7 +1038,7 @@
Benchmark.benchmark_requirements(build_options)
if (build_context.jobs > 0) {
- val benchmark_options = build_options.string("build_hostname") = hostname
+ val benchmark_options = build_options.string.update("build_hostname", hostname)
Benchmark.benchmark(benchmark_options, progress)
}
_build_cluster.benchmark()
--- a/src/Pure/System/benchmark.scala Thu Feb 15 12:18:25 2024 +0100
+++ b/src/Pure/System/benchmark.scala Thu Feb 15 12:37:52 2024 +0100
@@ -25,7 +25,7 @@
def benchmark_requirements(options: Options, progress: Progress = new Progress()): Unit = {
val res =
Build.build(
- options.string("build_engine") = Build.Default_Engine().name,
+ options.string.update("build_engine", Build.Default_Engine().name),
selection = Sessions.Selection(requirements = true, sessions = List(benchmark_session)),
progress = progress, build_heap = true)
if (!res.ok) error("Failed building requirements")
@@ -41,7 +41,7 @@
progress.echo("Starting benchmark ...")
val selection = Sessions.Selection(sessions = List(benchmark_session))
- val full_sessions = Sessions.load_structure(options.int("threads") = 1)
+ val full_sessions = Sessions.load_structure(options.int.update("threads", 1))
val build_context =
Build.Context(store, new Build.Default_Engine,
--- a/src/Pure/System/host.scala Thu Feb 15 12:18:25 2024 +0100
+++ b/src/Pure/System/host.scala Thu Feb 15 12:37:52 2024 +0100
@@ -62,22 +62,22 @@
numa_node match {
case None => options
case Some(node) =>
- options.string("process_policy") = if (numactl_ok(node)) numactl(node) else ""
+ options.string.update("process_policy", if (numactl_ok(node)) numactl(node) else "")
}
def node_options(options: Options, node: Node_Info): Options = {
val threads_options =
- if (node.rel_cpus.isEmpty) options else options.int("threads") = node.rel_cpus.length
+ if (node.rel_cpus.isEmpty) options else options.int.update("threads", node.rel_cpus.length)
node.numa_node match {
case None if node.rel_cpus.isEmpty =>
threads_options
case Some(numa_node) =>
- threads_options.string("process_policy") =
- if (numactl_ok(numa_node, node.rel_cpus)) numactl(numa_node, node.rel_cpus) else ""
+ threads_options.string.update("process_policy",
+ if (numactl_ok(numa_node, node.rel_cpus)) numactl(numa_node, node.rel_cpus) else "")
case _ =>
- threads_options.string("process_policy") =
- if (taskset_ok(node.rel_cpus)) taskset(node.rel_cpus) else ""
+ threads_options.string.update("process_policy",
+ if (taskset_ok(node.rel_cpus)) taskset(node.rel_cpus) else "")
}
}
--- a/src/Tools/VSCode/src/language_server.scala Thu Feb 15 12:18:25 2024 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Thu Feb 15 12:37:52 2024 +0100
@@ -288,7 +288,7 @@
}
}
- val session_options = options.bool("editor_output_state") = true
+ val session_options = options.bool.update("editor_output_state", true)
val session = new Session(session_options, resources)
Some((session_background, session))