# HG changeset patch
# User wenzelm
# Date 1663838505 -7200
# Node ID 19978abbc1116e35d7df56871037971f7e007229
# Parent  a1f458f089b9421d882c8ccf56fe77bee32d0ab7
tuned;

diff -r a1f458f089b9 -r 19978abbc111 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Sep 22 10:38:52 2022 +0200
+++ b/src/Pure/Tools/build.scala	Thu Sep 22 11:21:45 2022 +0200
@@ -455,13 +455,15 @@
         }
         else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
 
-      new Results(
+      val results1 =
         (for ((name, result) <- results0.iterator)
-          yield (name, (result.process, result.info))).toMap)
+          yield (name, (result.process, result.info))).toMap
+
+      new Results(results1)
     }
 
     if (export_files) {
-      for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) {
+      for (name <- full_sessions_selection.iterator if results(name).ok) {
         val info = results.info(name)
         if (info.export_files.nonEmpty) {
           progress.echo("Exporting " + info.name + " ...")
@@ -475,7 +477,7 @@
       }
     }
 
-    if (results.rc != Process_Result.RC.ok && (verbose || !no_build)) {
+    if (!results.ok && (verbose || !no_build)) {
       val unfinished =
         (for {
           name <- results.sessions.iterator