minor performance tuning;
authorwenzelm
Fri, 31 May 2024 22:35:44 +0200
changeset 80223 d389577a6fba
parent 80222 18a36de467bc
child 80224 db92e0b6a11a
minor performance tuning;
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)
   }
 }