# HG changeset patch
# User wenzelm
# Date 1689778584 -7200
# Node ID 64e5abd3a3a71cb953aa5878667dd5a5b575e34c
# Parent  c5170293d392ebf4a85156d81aacd6339cd261a4
tuned;

diff -r c5170293d392 -r 64e5abd3a3a7 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Jul 19 16:48:22 2023 +0200
+++ b/src/Pure/Tools/build.scala	Wed Jul 19 16:56:24 2023 +0200
@@ -464,7 +464,6 @@
   def build_worker(
     options: Options,
     build_id: String = "",
-    worker_id: String = "",
     progress: Progress = new Progress,
     list_builds: Boolean = false,
     dirs: List[Path] = Nil,
@@ -524,7 +523,7 @@
 Usage: isabelle build_worker [OPTIONS]
 
   Options are:
-    -B UUID      identify build process: mandatory for multiple active builds
+    -B UUID      existing UUID for build process (default: from database)
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -d DIR       include session directory
     -j INT       maximum number of parallel jobs (default 1)
@@ -547,7 +546,8 @@
 
       val res =
         progress.interrupt_handler {
-          build_worker(options, build_id,
+          build_worker(options,
+            build_id = build_id,
             progress = progress,
             list_builds = list_builds,
             dirs = dirs.toList,