--- 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))
}