# HG changeset patch
# User wenzelm
# Date 1676980914 -3600
# Node ID c81abb66a97f7d3162552bec86dbdd2885cb4d60
# Parent  0a91c697a18a45a2c2bdd478d0387ca0a44d58e9
tuned signature;

diff -r 0a91c697a18a -r c81abb66a97f src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Feb 21 12:58:19 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Feb 21 13:01:54 2023 +0100
@@ -441,7 +441,7 @@
         for (job <- finished_running()) finish_job(job)
 
         next_pending() match {
-          case Some(session_name) => start_job(session_name)
+          case Some(name) => start_job(name)
           case None => sleep()
         }
       }