author | wenzelm |
Sun, 27 Aug 2023 12:49:43 +0200 | |
changeset 78583 | 8f11794211ef |
parent 78582 | 63f06b935a1f |
child 78584 | 92ef737f412c |
--- a/src/Pure/General/ssh.scala Sat Aug 26 13:48:14 2023 +0200 +++ b/src/Pure/General/ssh.scala Sun Aug 27 12:49:43 2023 +0200 @@ -97,7 +97,7 @@ port: Int = 0, user: String = "" ): Session = { - require(!is_local(host), "Illegal host name " + quote(host)) + if (is_local(host)) error("Illegal SSH host name " + quote(host)) val multiplex = options.bool("ssh_multiplexing") && !Platform.is_windows val (control_master, control_path) =