# 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 }