--- 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 {