tuned error;
authorwenzelm
Sun, 27 Aug 2023 12:49:43 +0200
changeset 78583 8f11794211ef
parent 78582 63f06b935a1f
child 78584 92ef737f412c
tuned error;
src/Pure/General/ssh.scala
--- 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) =