# HG changeset patch
# User wenzelm
# Date 1717187744 -7200
# Node ID d389577a6fbaf4f92337a20c054af04b0ce09d07
# Parent  18a36de467bcf5c0c345895e1cdcee7da54e5cdb
minor performance tuning;

diff -r 18a36de467bc -r d389577a6fba src/Pure/System/other_isabelle.scala
--- a/src/Pure/System/other_isabelle.scala	Fri May 31 22:19:31 2024 +0200
+++ b/src/Pure/System/other_isabelle.scala	Fri May 31 22:35:44 2024 +0200
@@ -183,7 +183,6 @@
 
   def cleanup(): Unit = {
     clean_settings()
-    ssh.delete(etc)
-    ssh.delete(isabelle_home_user)
+    ssh.delete(etc, isabelle_home_user)
   }
 }