# HG changeset patch
# User wenzelm
# Date 1708077109 -3600
# Node ID 73b8ac4b0492b9aea800f33d73b16f847937ead2
# Parent  96bfb554b216425b964f299d54c59eb253e15046
tuned signature;

diff -r 96bfb554b216 -r 73b8ac4b0492 src/Pure/Build/build_cluster.scala
--- a/src/Pure/Build/build_cluster.scala	Fri Feb 16 10:45:24 2024 +0100
+++ b/src/Pure/Build/build_cluster.scala	Fri Feb 16 10:51:49 2024 +0100
@@ -101,7 +101,7 @@
     }
 
     def parse_single(registry: Registry, str: String): Host =
-      Library.the_single(parse(registry, str), "Single host expected: " + quote(str))
+      Library.the_single(parse(registry, str), message = "Single host expected: " + quote(str))
   }
 
   class Host(