# HG changeset patch # User Fabian Huch # 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) }) }