# HG changeset patch # User wenzelm # Date 1663017890 -7200 # Node ID 497e105a4618f42421892eaf0bdc150d2f3d2b48 # Parent 7057bf084ea56c0fc0ced56a7a5575f65e4206ff clarified error; diff -r 7057bf084ea5 -r 497e105a4618 src/Pure/General/ssh.scala --- 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 {