# HG changeset patch
# User wenzelm
# Date 1676977873 -3600
# Node ID 1a5ee9b70de9a33516eafb3f1a10c160a43c978a
# Parent  38643c64b1e2dd5dc86df0bbab1ce2cfb81de9b0
tuned signature;

diff -r 38643c64b1e2 -r 1a5ee9b70de9 src/Pure/Tools/build_process.scala
--- 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)