author | wenzelm |
Fri, 14 Jul 2023 11:11:06 +0200 | |
changeset 78339 | f8a553a21423 |
parent 78332 | 3b4bbc5b7c46 |
child 78340 | 5790e48f7573 |
--- a/src/Pure/General/ssh.scala Fri Jul 14 09:32:44 2023 +0200 +++ b/src/Pure/General/ssh.scala Fri Jul 14 11:11:06 2023 +0200 @@ -317,7 +317,7 @@ /* port forwarding */ def port_forwarding( - remote_port: Int, + remote_port: Int = 0, remote_host: String = "localhost", local_port: Int = 0, local_host: String = "localhost",