tuned signature;
authorwenzelm
Fri, 16 Feb 2024 10:51:49 +0100
changeset 79626 73b8ac4b0492
parent 79625 96bfb554b216
child 79627 0f01c575ff3e
tuned signature;
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(