# HG changeset patch
# User wenzelm
# Date 1689620390 -7200
# Node ID 4d9b953c7026548b3c5c4c9c78948181a8234d36
# Parent  6b6a3e7a0d32b2d2bbadd005e00a4a02c8f07f68
tuned signature;

diff -r 6b6a3e7a0d32 -r 4d9b953c7026 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Jul 17 20:44:58 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Mon Jul 17 20:59:50 2023 +0200
@@ -1079,7 +1079,7 @@
         build_options.seconds("build_delay").sleep()
       }
 
-    def start_job(): Boolean = synchronized_database("Build_Process.start_job") {
+    def check_job(): Boolean = synchronized_database("Build_Process.check_job") {
       next_job(_state) match {
         case Some(name) =>
           if (is_session_name(name)) {
@@ -1118,7 +1118,7 @@
             }
           }
 
-          if (!start_job()) sleep()
+          if (!check_job()) sleep()
         }
       }
       finally {