# HG changeset patch
# User wenzelm
# Date 1670783691 -3600
# Node ID 3bacdff9e24f69bc7d47dbbcb8a3ca6b1ba417b1
# Parent  247a51c3abec5e402eed092d5465d7bcd5616b60
tuned implementation;

diff -r 247a51c3abec -r 3bacdff9e24f src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Dec 11 18:57:41 2022 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Dec 11 19:34:51 2022 +0100
@@ -175,11 +175,9 @@
   }
 
   def with_copy_dir[A](dir1: Path, dir2: Path)(body: => A): A = {
-    if (dir2.is_file || dir2.is_dir) error("Directory already exists: " + dir2.absolute)
-    else {
-      try { copy_dir(dir1, dir2); body }
-      finally { rm_tree(dir2) }
-    }
+    new_directory(dir2)
+    try { copy_dir(dir1, dir2, direct = true); body }
+    finally { rm_tree(dir2) }
   }