ssh_config: Hostname with multiple IP addresses

[Brian Candler]

On 11/12/2020 08:42, Harald Dunkel wrote:
> ssh_config(5) explicitly allows numeric IP addresses (plural) on the
> Hostname config line in .ssh/config,

Can you point to where it says that explicitly? I see in ssh_config(5):

      HostName
              Specifies the real host name to log into.

Note that "real host name" is in the singular.

It then does make use of the plural:

      This can be used to specify nicknames or abbreviations for hosts

but I read that as meaning that you can configure multiple hosts, each 
with its own HostName, e.g.

Host foo
HostName 192.0.2.1

Host bar
HostName 192.0.2.2

Similarly:

      Arguments to HostName accept the tokens described in the TOKENS 
section.  Numeric IP addresses are also permitted

To me this is talking about multiple HostName entries in the same 
ssh_config file, each belonging to a different Host, rather than one 
HostName allowing multiple IP addresses. However I guess it could be 
read either way.