# HG changeset patch
# User wenzelm
# Date 1670763256 -3600
# Node ID 87d0aab3a8e47f431137b744e20ff0a5b51e6b20
# Parent  aeded421d37449bee2cded50bcfb5c532661ebc4
tuned whitespace;

diff -r aeded421d374 -r 87d0aab3a8e4 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Dec 11 13:46:34 2022 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Dec 11 13:54:16 2022 +0100
@@ -173,7 +173,7 @@
     if (dir2.is_file || dir2.is_dir) error("Directory already exists: " + dir2.absolute)
     else {
       try { copy_dir(dir1, dir2); body }
-      finally { rm_tree(dir2 ) }
+      finally { rm_tree(dir2) }
     }
   }