changeset 77339 | c81abb66a97f |
parent 77338 | 0a91c697a18a |
child 77343 | db479840d6ad |
--- 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() } }