tuned output;
authorwenzelm
Thu, 30 Mar 2023 15:31:55 +0200
changeset 77761 04a250facd44
parent 77760 34178d26a360
child 77762 f73400337c5c
tuned output;
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 = ""