# 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,