src/Pure/Tools/build_process.scala
changeset 77332 1a5ee9b70de9
parent 77331 38643c64b1e2
child 77333 0bec014c0f9f
--- 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)