author | wenzelm |
Fri, 21 Jul 2023 11:11:50 +0200 | |
changeset 78423 | 645b54f3244a |
parent 78422 | dcaf6f33d94d |
child 78424 | e5908be41a36 |
--- a/src/Pure/Tools/build_cluster.scala Fri Jul 21 11:05:50 2023 +0200 +++ b/src/Pure/Tools/build_cluster.scala Fri Jul 21 11:11:50 2023 +0200 @@ -50,7 +50,7 @@ val l = if (m == n) n else if (str(m) == ':') m + 1 - else error("Colon (:) expected after host name") + else error("Missing \":\" after host name") str.substring(l) } val (specs1, specs2) = Options.parse_specs(rest).partition(is_parameter)