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