# HG changeset patch
# User wenzelm
# Date 1689930710 -7200
# Node ID 645b54f3244a5738843dd41aacf9a76453bf5024
# Parent  dcaf6f33d94d686805a48f5160a05778e200e59c
tuned output;

diff -r dcaf6f33d94d -r 645b54f3244a 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)