SSH bookmarks - config file

Hi,

I've been testing the SSH bookmark feature, I like it - allows you to easily transport those host/keys (basically your SSH config) between machines without having to remember to copy it.

I don't like to click too much to open an SSH terminal - I prefer using command line.

As such, the current ssh bookmarks "generate config" is missing some fields to make it really useful: the port mostly - it does not save it in the generated configuration file, so you'd still need to go and copy the section over and modify it to your liking.

An SSH port seems like a basic thing to add - could it be considered?

When looking over my existing .ssh/config, I find I use
* host (which can be whatever alias you want)
* hostname (the actual host to connect to)
* username (used to connect to the remote machine)
* identity file (ssh pubkey)
* port

a lot.