# HG changeset patch
# User wenzelm
# Date 1717162708 -7200
# Node ID 3a88980070383787fd655a597e2700f24777a9ce
# Parent  c6d18c836509ab1ca9e58bb189a371279fafcaab
tuned;

diff -r c6d18c836509 -r 3a8898007038 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri May 31 15:26:17 2024 +0200
+++ b/src/Pure/General/ssh.scala	Fri May 31 15:38:28 2024 +0200
@@ -330,9 +330,8 @@
       Path.explode(execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out)
 
     override def with_tmp_dir[A](body: Path => A): A = {
-      val dir = tmp_dir()
-      try { body(dir) }
-      finally { rm_tree(dir) }
+      val path = tmp_dir()
+      try { body(path) } finally { rm_tree(path) }
     }