From 4c667d69c116eb5cbc9f4d7b6b7fbe30608ea86a Mon Sep 17 00:00:00 2001
From: gpancot <gpancot@hotmail.com>
Date: Mon, 16 Jan 2023 14:53:08 +0100
Subject: [PATCH] allow different port from ssh_config

---
 src/server/command/ssh.ts | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/server/command/ssh.ts b/src/server/command/ssh.ts
index 0a04c72f..b01bdd47 100644
--- a/src/server/command/ssh.ts
+++ b/src/server/command/ssh.ts
@@ -21,9 +21,10 @@ export function sshOptions(
   if (!isUndefined(config) && config !== '') {
     sshRemoteOptsBase = sshRemoteOptsBase.concat(['-F', config]);
   }
+  if (!isUndefined(port) && port !== '') {
+      sshRemoteOptsBase = sshRemoteOptsBase.concat(['-p', port]);
+  }
   sshRemoteOptsBase = sshRemoteOptsBase.concat([
-    '-p',
-    port,
     '-o',
     `PreferredAuthentications=${auth}`,
     '-o',