If the option is not provided, ssh uses the default port for the host,
which is usually 22, but may be overridden in the user's SSH
configuration.
Change-Id: I303e9aeae16bd73a96c5e6d54f8e39482613db28
Signed-off-by: Jonathan Neuschäfer <j.neuschaefer@gmx.net>
Reviewed-on: https://review.coreboot.org/14522
Tested-by: build bot (Jenkins)
Reviewed-by: David Hendricks <dhendrix@chromium.org>
4aef682819