changeset 80109 | dbcd6dc7f70f |
parent 80056 | 9279e96eb34e |
child 80118 | 0323cd9fcab9 |
--- a/src/Pure/Build/build_schedule.scala Thu Apr 11 12:04:44 2024 +0200 +++ b/src/Pure/Build/build_schedule.scala Thu Apr 11 12:05:01 2024 +0200 @@ -471,8 +471,9 @@ if (used.length >= host.max_jobs) false else { - if (host.numa_nodes.length <= 1) + if (host.numa_nodes.length <= 1) { used.map(host_infos.num_threads).sum + threads <= host.max_threads + } else { def node_threads(n: Int): Int = used.filter(_.numa_node.contains(n)).map(host_infos.num_threads).sum