tuned output;
authorwenzelm
Fri, 21 Jul 2023 11:11:50 +0200
changeset 78423 645b54f3244a
parent 78422 dcaf6f33d94d
child 78424 e5908be41a36
tuned output;
src/Pure/Tools/build_cluster.scala
--- 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)