# HG changeset patch
# User wenzelm
# Date 1663102902 -7200
# Node ID 35a279a2d24606e3e49593df851469aa8579e26a
# Parent  e8d4013c49d1b9f924de52aab4f4887db3cb3e8f
clarified signature;

diff -r e8d4013c49d1 -r 35a279a2d246 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Sep 13 22:36:41 2022 +0200
+++ b/src/Pure/General/ssh.scala	Tue Sep 13 23:01:42 2022 +0200
@@ -82,11 +82,7 @@
     multiplex: Boolean = !Platform.is_windows
   ): Session = {
     val (control_master, control_path) =
-      if (multiplex) {
-        val file = Isabelle_System.tmp_file("ssh_socket")
-        file.delete()
-        (true, file.getPath)
-      }
+      if (multiplex) (true, Isabelle_System.tmp_file("ssh_socket", initialized = false).getPath)
       else (false, "")
 
     new Session(options, host, port, user, control_master, control_path)
diff -r e8d4013c49d1 -r 35a279a2d246 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Sep 13 22:36:41 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Sep 13 23:01:42 2022 +0200
@@ -269,10 +269,15 @@
     File.platform_file(path)
   }
 
-  def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = {
+  def tmp_file(
+    name: String,
+    ext: String = "",
+    base_dir: JFile = isabelle_tmp_prefix(),
+    initialized: Boolean = true
+  ): JFile = {
     val suffix = if (ext == "") "" else "." + ext
     val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
-    file.deleteOnExit()
+    if (initialized) file.deleteOnExit() else file.delete()
     file
   }