src/Pure/General/ssh.scala
changeset 71383 8313dca6dee9
parent 71358 ec48da635e6c
child 71549 319599ba28cf
--- a/src/Pure/General/ssh.scala	Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/General/ssh.scala	Wed Jan 15 19:54:50 2020 +0100
@@ -90,7 +90,7 @@
       host_key_alias: String = "",
       on_close: () => Unit = () => ()): Session =
     {
-      val session = jsch.getSession(proper_string(user) getOrElse null, host, make_port(port))
+      val session = jsch.getSession(proper_string(user).orNull, host, make_port(port))
 
       session.setUserInfo(No_User_Info)
       session.setServerAliveInterval(alive_interval(options))