tuned;
authorwenzelm
Wed, 01 Mar 2023 16:01:01 +0100
changeset 77452 9016252f9470
parent 77451 0093124710db
child 77453 e72b1f5fd88d
tuned;
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 15:45:58 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 16:01:01 2023 +0100
@@ -597,7 +597,15 @@
           make_result(session_name, false, output_heap, Process_Result.error)
       }
     }
-    else if (ancestor_results.forall(_.ok) && !progress.stopped) {
+    else if (!ancestor_results.forall(_.ok) || progress.stopped) {
+      progress.echo(session_name + " CANCELLED")
+      synchronized {
+        _state = _state.
+          remove_pending(session_name).
+          make_result(session_name, false, output_heap, Process_Result.undefined)
+      }
+    }
+    else {
       progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
 
       store.clean_output(session_name)
@@ -628,14 +636,6 @@
         }
       job.start()
     }
-    else {
-      progress.echo(session_name + " CANCELLED")
-      synchronized {
-        _state = _state.
-          remove_pending(session_name).
-          make_result(session_name, false, output_heap, Process_Result.undefined)
-      }
-    }
   }