# 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 {