# HG changeset patch
# User wenzelm
# Date 1708257660 -3600
# Node ID 49475f8bb4cc2ac0b6e2ad2ae2d9d18dd2e67697
# Parent  a4118f5302639b8bacd30ea150e8ee30ff8572b9
tuned: afford untyped/unscoped update;

diff -r a4118f530263 -r 49475f8bb4cc src/Pure/Admin/ci_build.scala
--- a/src/Pure/Admin/ci_build.scala	Sun Feb 18 12:33:43 2024 +0100
+++ b/src/Pure/Admin/ci_build.scala	Sun Feb 18 13:01:00 2024 +0100
@@ -127,10 +127,7 @@
 
   private def with_documents(options: Options, config: Build_Config): Options = {
     if (config.documents) {
-      options
-        .bool.update("browser_info", true)
-        .string.update("document", "pdf")
-        .string.update("document_variants", "document:outline=/proof,/ML")
+      options + "browser_info" + "document=pdf" + "document_variants=document:outline=/proof,/ML"
     }
     else options
   }
@@ -156,10 +153,8 @@
     println(Build_Log.Settings.show())
 
     val build_options =
-      with_documents(options, config)
-        .int.update("parallel_proofs", 1)
-        .int.update("threads", profile.threads)
-        + "system_heaps"
+      with_documents(options, config).int.update("threads", profile.threads) +
+        "parallel_proofs=1" + "system_heaps"
 
     println(s"jobs = ${profile.jobs}, threads = ${profile.threads}, numa = ${profile.numa}")
 
diff -r a4118f530263 -r 49475f8bb4cc src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Sun Feb 18 12:33:43 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Sun Feb 18 13:01:00 2024 +0100
@@ -54,10 +54,7 @@
         val heaps = session.ancestors.map(store.output_heap)
         ML_Heap.restore(database_server, heaps, cache = store.cache.compress)
 
-        val local_options =
-          options
-            .bool.update("build_database_server", false)
-            .bool.update("build_database", false)
+        val local_options = options + "build_database_server=false" + "build_database=false"
 
         benchmark_requirements(local_options, progress)
         ML_Heap.restore(database_server, heaps, cache = store.cache.compress)