--- a/src/Pure/General/ssh.scala Thu Mar 30 14:25:31 2023 +0200
+++ b/src/Pure/General/ssh.scala Thu Mar 30 15:31:55 2023 +0200
@@ -109,6 +109,7 @@
def user_prefix: String = if (user.nonEmpty) user + "@" else ""
override def toString: String = user_prefix + host + port_suffix
+ override def print: String = " (ssh " + toString + ")"
override def hg_url: String = "ssh://" + toString + "/"
override def rsync_prefix: String = user_prefix + host + ":"
@@ -371,6 +372,8 @@
trait System extends AutoCloseable {
def close(): Unit = ()
+ override def toString: String = "SSH.Local"
+ def print: String = ""
def hg_url: String = ""
def rsync_prefix: String = ""