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
Original-Signed-off-by: Jonathan Neuschäfer <j.neuschaefer@gmx.net>
Original-Reviewed-on: https://review.coreboot.org/14522
Original-Reviewed-by: David Hendricks <dhendrix@chromium.org>
(cherry-picked from commit 4aef682819)
Signed-off-by: Martin Roth <martinroth@chromium.org>
Reviewed-on: https://chromium-review.googlesource.com/346465
Reviewed-by: Stefan Reinauer <reinauer@google.com>
Commit-Queue: Stefan Reinauer <reinauer@google.com>
Tested-by: Stefan Reinauer <reinauer@google.com>
5324d40651