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