4aef682819
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>