# HG changeset patch
# User wenzelm
# Date 1476088934 -7200
# Node ID cc5ea4d648d85c8b223e76970b4e072d2c3eff4c
# Parent  14782d58a5038e9e41b737b2e5ba820124a28d34
tuned;

diff -r 14782d58a503 -r cc5ea4d648d8 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Oct 10 10:41:04 2016 +0200
+++ b/src/Pure/General/ssh.scala	Mon Oct 10 10:42:14 2016 +0200
@@ -60,6 +60,19 @@
   }
 
 
+  /* user info */
+
+  object No_User_Info extends UserInfo
+  {
+    def getPassphrase: String = null
+    def getPassword: String = null
+    def promptPassword(msg: String): Boolean = false
+    def promptPassphrase(msg: String): Boolean = false
+    def promptYesNo(msg: String): Boolean = false
+    def showMessage(msg: String): Unit = Output.writeln(msg)
+  }
+
+
   /* session */
 
   class Session private[SSH](val session: JSch_Session)
@@ -78,16 +91,6 @@
     def channel_sftp: ChannelSftp =
       session.openChannel("sftp").asInstanceOf[ChannelSftp]
   }
-
-  object No_User_Info extends UserInfo
-  {
-    def getPassphrase: String = null
-    def getPassword: String = null
-    def promptPassword(msg: String): Boolean = false
-    def promptPassphrase(msg: String): Boolean = false
-    def promptYesNo(msg: String): Boolean = false
-    def showMessage(msg: String): Unit = Output.writeln(msg)
-  }
 }
 
 class SSH private(val jsch: JSch)