Custom ports in SSH config for VSCode Remote SSH

Scenario

You want to connect to a remote workstation via VsCode, but on a different port than the default (22).

Why would you need to do this?
There could be any reason, but one that comes to mind is if the default port requires authentication using something like PAM, or Kerberos, and you only want to be bothered by entering passwords when you use the default port instead of a custom port.

Problem

By default the Vscode Remote SSH plugin uses your local ~/.ssh/config file for configuring remote connections. Let's assume that in that file, you have created a host configuration like:

Host my-company-machine
   User my-user-name
   HostName 127.0.0.1
   GSSAPIAuthentication yes

Now you would like to connect to the remote machine through VSCode's Remote SSH extension, but using a different port than the default.

Ok solution

The easy solution would be to just add the port to the config file like so:

Host my-company-machine
   User my-user-name
   HostName 127.0.0.1
   GSSAPIAuthentication no
   Port 5000

Now VScode can connect to my-company-name using port 5000 on the remote, and problem solved?

Not really because we've now removed the authentication method required for the default port.

Better solution

The manpage for ssh_config(5) lists a directive called Include, which allows us to include other ssh configs inside ours.

Furthermore, we can override configuration for host declarations found in those other configs.

The solution I propose (and which has worked for me), is to create a new config for vscode, and in that file, override the port used to connect to the remote host.

~/.ssh/config

Host my-company-machine
   User my-user-name
   HostName 127.0.0.1
   GSSAPIAuthentication yes

~/.ssh/vscode-config

Host my-company-machine
   GSSAPIAuthentication no
   Port 5000
Include ~/.ssh/config

Now you just need to change your plugin settings so that VSCode uses this new config, instead of your default one. Next time you connect to the remote host, VSCode will use port 5000, and when you connect via regular ssh from a terminal, you will use port 22 by default, (or specify a custom port via the -p option).