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