src/Pure/Tools/build_process.scala
changeset 77464 8008ce0f2488
parent 77463 4e8bec105ce5
child 77465 ecfe6dac3a3e
--- 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()