# HG changeset patch
# User wenzelm
# Date 1680183115 -7200
# Node ID 04a250facd44a68457b878d3187b18c7bfc0917f
# Parent  34178d26a360be58a4606f9b263c8b602ca6421a
tuned output;

diff -r 34178d26a360 -r 04a250facd44 src/Pure/General/ssh.scala
--- 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 = ""