Feature: SSH into docker containers without extra ssh server running

[robin-mueller]

Add support for directly establishing a ssh connection with a docker container without the need of an extra ssh server.

[StefanFabian]

Looks mostly good but the ssh server on the remote PC could be running on a port different from 22 which is not handled here.
Not entirely sure where to put the port in the docker host argument though, did you try using ssh directly?

[robin-mueller]

Yes, that's important to consider. According to the docs, it's pretty easy to add the port to the docker host specifier, so I would stick to using the docker command.

I've added a commit, so now it should be more robust.

[robin-mueller]

BTW: ssh user@host docker exec -it container-name /bin/bash doesn't work because ssh doesn't provide a TTY:

the input device is not a TTY

[StefanFabian]

I am a bit hesitant if this makes sense as part of the command.
The ssh command is only a convenience command, so you don't have to write hector robots ROBOT_NAME PC_NAME ssh.
And especially the case where you specify a robot and not a PC, where it would use all PCs, doesn't make sense with the container argument, because it is not a common setup that all robot PCs have the same Docker container running.

I would suggest creating an overlay and creating this feature as a custom command in the form of a script in that overlay.