clarified error;
authorwenzelm
Mon, 12 Sep 2022 23:24:50 +0200
changeset 76125 497e105a4618
parent 76124 7057bf084ea5
child 76126 a284c752db39
clarified error;
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 {