I confirm that works. Thank you for your help with this.

On Mon, Feb 10, 2025 at 10:40 AM Michael Albinus <michael.albinus@gmx.de>
wrote:

> Ship Mints <shipmints@gmail.com> writes:
>
> Hi,
>
> > I also alias host names in ssh config, yep. It's very common for the
> > ssh "spec" and the reported host name to be different. The ansi
> > sequences must be respected in these cases.
>
> Understood. Finally, I've pushed a fix to master w/o checking host
> names. Pls see whether this works as expected.
>
> Best regards, Michael.
>