# HG changeset patch
# User wenzelm
# Date 1708201708 -3600
# Node ID cff4576218fa0b29f7a6bd8afa7de9c41860c827
# Parent  10e560f2f580b5afe3724d4871363033bd64fa2d
tuned: afford untyped/unscoped update;

diff -r 10e560f2f580 -r cff4576218fa src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Sat Feb 17 21:26:00 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Sat Feb 17 21:28:28 2024 +0100
@@ -43,7 +43,7 @@
 
         progress.echo("Starting benchmark ...")
         val selection = Sessions.Selection(sessions = List(benchmark_session))
-        val full_sessions = Sessions.load_structure(options.int.update("threads", 1))
+        val full_sessions = Sessions.load_structure(options + "threads=1")
 
         val build_deps = Sessions.deps(full_sessions.selection(selection)).check_errors
         val build_context = Build.Context(store, build_deps, jobs = 1)