author | wenzelm |
Mon, 12 Sep 2022 23:24:50 +0200 | |
changeset 76125 | 497e105a4618 |
parent 76124 | 7057bf084ea5 |
child 76126 | a284c752db39 |
--- a/src/Pure/General/ssh.scala Mon Sep 12 23:10:45 2022 +0200 +++ b/src/Pure/General/ssh.scala Mon Sep 12 23:24:50 2022 +0200 @@ -266,6 +266,8 @@ local_host: String = "localhost", ssh_close: Boolean = false ): Port_Forwarding = { + if (control_path.isEmpty) error("SSH port forwarding requires multiplexing") + val port = if (local_port > 0) local_port else {