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))