diff -r 678e00851cfb -r 556c34fd0554 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu May 04 14:57:31 2017 +0200
+++ b/src/Pure/General/ssh.scala	Thu May 04 14:58:19 2017 +0200
@@ -77,7 +77,8 @@
     def open_session(host: String, user: String = "", port: Int = 0): Session =
     {
       val session =
-        jsch.getSession(if (user == "") null else user, host, if (port > 0) port else default_port)
+        jsch.getSession(proper_string(user) getOrElse null, host,
+          if (port > 0) port else default_port)
 
       session.setUserInfo(No_User_Info)
       session.setServerAliveInterval(alive_interval(options))