tuned;
authorwenzelm
Fri, 16 Feb 2024 15:17:30 +0100
changeset 79632 463f94c504a4
parent 79629 4d81c0391da2
child 79633 c59231722f10
tuned;
src/Pure/Build/build_cluster.scala
--- a/src/Pure/Build/build_cluster.scala	Fri Feb 16 11:25:11 2024 +0100
+++ b/src/Pure/Build/build_cluster.scala	Fri Feb 16 15:17:30 2024 +0100
@@ -131,7 +131,7 @@
           if (host.port == 0) "" else Options.Spec.print(Host.PORT, host.port.toString),
           if (host.jobs == 1) "" else Options.Spec.print(Host.JOBS, host.jobs.toString),
           if_proper(host.numa, Host.NUMA),
-          if_proper(dirs, Options.Spec.print(Host.DIRS, host.dirs)),
+          if_proper(host.dirs, Options.Spec.print(Host.DIRS, host.dirs)),
           if_proper(host.shared, Host.SHARED)
         ).filter(_.nonEmpty)
       val rest = (params ::: host.options.map(_.print)).mkString(",")