# HG changeset patch # User wenzelm # Date 1754821659 -7200 # Node ID 9c34a176817897477bd3fac837408beb534b7208 # Parent 889d5cdc034b076580b237e5b5649b269519a266 tuned signature; diff -r 889d5cdc034b -r 9c34a1768178 src/Pure/Build/build.scala --- a/src/Pure/Build/build.scala Sat Aug 09 20:22:19 2025 +0200 +++ b/src/Pure/Build/build.scala Sun Aug 10 12:27:39 2025 +0200 @@ -195,7 +195,7 @@ val full_sessions = Sessions.load_structure(build_options, dirs = AFP.main_dirs(afp_root) ::: dirs, select_dirs = select_dirs, infos = infos, augment_options = augment_options) - val full_sessions_selection = full_sessions.imports_selection(selection) + val selected_sessions = full_sessions.imports_selection(selection) val build_deps = { val deps0 = @@ -247,7 +247,7 @@ /* build process and results */ val clean_sessions = - if (clean_build) full_sessions.imports_descendants(full_sessions_selection) else Nil + if (clean_build) full_sessions.imports_descendants(selected_sessions) else Nil val numa_nodes = Host.numa_nodes(enabled = numa_shuffling) val build_context = @@ -261,7 +261,7 @@ val results = engine.run_build_process(build_context, progress, server) if (export_files) { - for (name <- full_sessions_selection.iterator if results(name).ok) { + for (name <- selected_sessions.iterator if results(name).ok) { val info = results.info(name) if (info.export_files.nonEmpty) { progress.echo("Exporting " + info.name + " ...")