# HG changeset patch # User wenzelm # Date 1708187607 -3600 # Node ID 155bb0ae4ae228e4842a5bd5fdc970a3ea84a1a2 # Parent 65ef68bab8d6eed405cda3409ce044de0dfa8697 more robust: disallow empty clusters, so "isabelle build -H" really means cluster build; diff -r 65ef68bab8d6 -r 155bb0ae4ae2 src/Pure/System/registry.scala --- a/src/Pure/System/registry.scala Sat Feb 17 17:23:22 2024 +0100 +++ b/src/Pure/System/registry.scala Sat Feb 17 17:33:27 2024 +0100 @@ -84,8 +84,8 @@ override def table_value(registry: Registry, t: TOML.Table, a: String): Value = { val hosts = t.array.get(prefix_hosts) match { - case Some(arr) => arr.string.values.map(_.rep) - case None => bad_value(Long_Name.qualify(a, prefix_hosts)) + case Some(arr) if arr.length > 0 => arr.string.values.map(_.rep) + case _ => bad_value(Long_Name.qualify(a, prefix_hosts)) } val cluster_specs = Host_Cluster.get(registry, a) hosts.map(h => (h, Host_Strict.get(registry, h) ::: cluster_specs))