diff -r 4e8bec105ce5 -r 8008ce0f2488 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Wed Mar 01 21:07:59 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Wed Mar 01 21:15:20 2023 +0100 @@ -551,7 +551,7 @@ } else None - protected def start_job(session_name: String): Unit = { + protected def start_session(session_name: String): Unit = { val ancestor_results = synchronized { _state.get_results(build_context.sessions(session_name).ancestors) } @@ -671,7 +671,8 @@ synchronized { next_job(_state) } match { case Some(name) => - start_job(name) + if (Build_Job.is_session_name(name)) start_session(name) + else error("Unsupported build job name " + quote(name)) case None => sync_database() sleep()