# HG changeset patch # User wenzelm # Date 1520348254 -3600 # Node ID 3b91c21dcb003188dce54a2b460344ef6ab58984 # Parent 25f3a278df3de2d5e206f15b274086c8fb24592d tuned signature; diff -r 25f3a278df3d -r 3b91c21dcb00 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Tue Mar 06 15:51:34 2018 +0100 +++ b/src/Pure/General/ssh.scala Tue Mar 06 15:57:34 2018 +0100 @@ -75,9 +75,11 @@ } def open_session(options: Options, host: String, user: String = "", port: Int = 0, - proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0): Session = + proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, + permissive: Boolean = false): Session = init_context(options).open_session(host = host, user = user, port = port, - proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port) + proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port, + permissive = permissive) class Context private[SSH](val options: Options, val jsch: JSch) {