tuned signature;
authorwenzelm
Tue, 06 Mar 2018 15:57:34 +0100
changeset 67771 3b91c21dcb00
parent 67770 25f3a278df3d
child 67772 71a318559e30
tuned signature;
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)
   {