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