# HG changeset patch # User wenzelm # Date 1716991697 -7200 # Node ID 67b5e8b887285086b6adfe7fd701d812348706e7 # Parent 2ec1b11f1f9309c82a37b1b100d26e6c964fa278 tuned tmp name; diff -r 2ec1b11f1f93 -r 67b5e8b88728 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Wed May 29 16:06:07 2024 +0200 +++ b/src/Pure/General/ssh.scala Wed May 29 16:08:17 2024 +0200 @@ -165,7 +165,7 @@ init: Path => Unit = _ => (), exit: Path => Unit = _ => () ): Process_Result = { - Isabelle_System.with_tmp_dir("ssh") { dir => + Isabelle_System.with_tmp_dir("sftp") { dir => init(dir) File.write(dir + Path.explode("script"), script) val result =