# HG changeset patch
# User wenzelm
# Date 1662749298 -7200
# Node ID 758fd2fbde1e0ca57df868e3f3105227237157a7
# Parent  101547fb2f78ab4bcfb2e46e96945806f2976ddb
unused;

diff -r 101547fb2f78 -r 758fd2fbde1e src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri Sep 09 20:20:06 2022 +0200
+++ b/src/Pure/General/ssh.scala	Fri Sep 09 20:48:18 2022 +0200
@@ -97,8 +97,6 @@
       permissive = permissive)
 
   class Context private[SSH](val options: Options, val jsch: JSch) {
-    def update_options(new_options: Options): Context = new Context(new_options, jsch)
-
     private def connect_session(
       host: String,
       user: String = "",
@@ -327,9 +325,6 @@
     val nominal_user: String,
     val nominal_port: Int
   ) extends System {
-    def update_options(new_options: Options): Session =
-      new Session(new_options, session, on_close, nominal_host, nominal_user, nominal_port)
-
     def host: String = if (session.getHost == null) "" else session.getHost
 
     override def hg_url: String =