src/Pure/Tools/build.scala
changeset 78411 64e5abd3a3a7
parent 78410 c5170293d392
child 78412 eda362f85cbf
--- 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,