# HG changeset patch
# User wenzelm
# Date 1693133383 -7200
# Node ID 8f11794211efa2ef7de3707003b9111624dae4e8
# Parent  63f06b935a1f244fbda8dd501f3c77d165d06b31
tuned error;

diff -r 63f06b935a1f -r 8f11794211ef 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) =