# HG changeset patch
# User wenzelm
# Date 1691689719 -7200
# Node ID 91817b2f3f55991c9a0580e234eba6ba94de28a2
# Parent  14da1177d1c380dda8dae1213330cbba60abe677
more robust wrt. undefined state;

diff -r 14da1177d1c3 -r 91817b2f3f55 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Aug 10 19:42:21 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Thu Aug 10 19:48:39 2023 +0200
@@ -1094,12 +1094,15 @@
       val jobs = next_jobs(_state)
       for (name <- jobs) {
         if (is_session_name(name)) {
-          _state.ancestor_results(name) match {
-            case Some(results) => _state = start_session(_state, name, results)
-            case None =>
-              build_progress.echo_warning(
-                "Broken build job " + quote(name) + ": no ancestor results")
+          if (build_context.sessions_structure.defined(name)) {
+            _state.ancestor_results(name) match {
+              case Some(results) => _state = start_session(_state, name, results)
+              case None =>
+                build_progress.echo_warning(
+                  "Broken build job " + quote(name) + ": no ancestor results")
+            }
           }
+          else build_progress.echo_warning("Broken build job " + quote(name) + ": no session info")
         }
         else build_progress.echo_warning("Unsupported build job " + quote(name))
       }