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