tuned signature;
authorwenzelm
Tue, 21 Feb 2023 13:01:54 +0100
changeset 77339 c81abb66a97f
parent 77338 0a91c697a18a
child 77340 35c1e34fc693
tuned signature;
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()
         }
       }