# HG changeset patch
# User wenzelm
# Date 1708093050 -3600
# Node ID 463f94c504a49ef90f714bd99d9980504ae09289
# Parent  4d81c0391da2af63638fa10be8eb7e288f429f6a
tuned;

diff -r 4d81c0391da2 -r 463f94c504a4 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(",")