Support specifying the port of a remote SSH connection

[planger]

What it does

Uses new URL(<host>) to parse the host specified by the user and pass on url.hostname and url.port when establishing the SSH connection. This way we enable users to specify the port of the remote SSH server.

Contributed on behalf of STMicroelectronics.
Fixes #13295

How to test

1. Start a container with open SSH server running and map it e.g. to port 2222 with docker run -d -p 2222:22 ssh-container
2. Run Connect to Host...
3. Enter user@localhost:2222
4. Observe how the establishing the connection now works

Test whether specifying no port, e.g. user@localhost still works.

Follow-ups

N/A

Review checklist

• As an author, I have thoroughly tested my changes and carefully followed the review guidelines

Reminder for reviewers

• As a reviewer, I agree to behave in accordance with the review guidelines

[msujew]

Thanks, looks good to me 👍