On Fri, 6 Sept 2024 at 20:40, Stuart Henderson <stu@spacehopper.org> wrote:
> An hostname as considered by ssh isn't necessarily a DNS hostname,
> for example people use aliases in .ssh/config. This does work for
> some chars not allowed in DNS, but I haven't been able to persuade
> it to work with @.

Ah, that is true. Thanks for paying attention.

I did not consider it because the hostnames in the case for which I
submitted the patch have to be expanded before, to retrieve the proper
host key and I'm not using any host pattern myself which would not
also work as regular hostname. So my mind was in the real hostname
space.