# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1719840327 -7200
# Node ID f2f4b953ead69a3c5e509ad4ffa62f2db32cf255
# Parent  a3bae6dd73448f9f2301cee61658a6112bcf5773
tuned;

diff -r a3bae6dd7344 -r f2f4b953ead6 etc/options
--- a/etc/options	Mon Jul 01 15:24:04 2024 +0200
+++ b/etc/options	Mon Jul 01 15:25:27 2024 +0200
@@ -244,6 +244,7 @@
   -- "isabelle identifier for build manager processes"
 
 option build_manager_cluster : string = "cluster.default"
+  -- "cluster for user-submitted tasks"
 
 option build_manager_timeout : real = 28800
   -- "timeout for user-submitted tasks (seconds > 0)"
diff -r a3bae6dd7344 -r f2f4b953ead6 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Mon Jul 01 15:24:04 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Mon Jul 01 15:25:27 2024 +0200
@@ -1679,12 +1679,11 @@
       val store = Store(options)
       val progress = new Console_Progress()
 
-      build_task(options, store = store, afp_root = afp_root, base_sessions =
-        base_sessions.toList, presentation = presentation, requirements = requirements,
-        exclude_session_groups = exclude_session_groups.toList, all_sessions = all_sessions,
-        build_heap = build_heap, clean_build = clean_build, export_files = export_files,
-        fresh_build = fresh_build, session_groups = session_groups.toList, sessions = sessions,
-        prefs = prefs.toList, verbose = verbose, rev = rev, exclude_sessions =
-        exclude_sessions.toList, progress = progress)
+      build_task(options, store, afp_root = afp_root, base_sessions = base_sessions.toList,
+        presentation = presentation, requirements = requirements, exclude_session_groups =
+        exclude_session_groups.toList, all_sessions = all_sessions, build_heap = build_heap,
+        clean_build = clean_build, export_files = export_files, fresh_build = fresh_build,
+        session_groups = session_groups.toList, sessions = sessions, prefs = prefs.toList, verbose =
+        verbose, rev = rev, exclude_sessions = exclude_sessions.toList, progress = progress)
     })
 }