--- a/src/Pure/Tools/build_process.scala Tue Feb 21 12:08:35 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Tue Feb 21 12:11:13 2023 +0100
@@ -199,7 +199,7 @@
protected var _running = Map.empty[String, Build_Job]
protected var _results = Map.empty[String, Build_Process.Result]
- protected def test_pending(): Boolean = synchronized { _pending.nonEmpty }
+ protected def is_pending(): Boolean = synchronized { _pending.nonEmpty }
protected def remove_pending(name: String): Unit = synchronized {
_pending = _pending.flatMap(entry => if (entry.name == name) None else Some(entry.resolve(name)))
@@ -401,8 +401,8 @@
}
def run(): Map[String, Process_Result] = {
- if (test_pending()) {
- while (test_pending()) {
+ if (is_pending()) {
+ while (is_pending()) {
if (progress.stopped) stop_running()
for (job <- finished_running()) finish_job(job)