diff -r 632a92fcb673 -r 6754b5eceb12 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun Feb 19 13:51:49 2023 +0100 +++ b/src/Pure/Tools/build.scala Mon Feb 20 10:29:45 2023 +0100 @@ -132,33 +132,23 @@ } val results = { - val build_results = - if (build_deps.is_empty) { - progress.echo_warning("Nothing to build") - Map.empty[String, Build_Process.Result] - } - else { - Isabelle_Thread.uninterruptible { - val build_process = - new Build_Process(build_context, build_heap = build_heap, - numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build, - no_build = no_build, verbose = verbose, session_setup = session_setup) - build_process.run() - } + val process_results = + Isabelle_Thread.uninterruptible { + val build_process = + new Build_Process(build_context, build_heap = build_heap, + numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build, + no_build = no_build, verbose = verbose, session_setup = session_setup) + build_process.run() } val sessions_ok: List[String] = (for { name <- build_deps.sessions_structure.build_topological_order.iterator - result <- build_results.get(name) + result <- process_results.get(name) if result.ok } yield name).toList - val results = - (for ((name, result) <- build_results.iterator) - yield (name, result.process_result)).toMap - - new Results(store, build_deps, sessions_ok, results) + new Results(store, build_deps, sessions_ok, process_results) } if (export_files) {