equal
deleted
inserted
replaced
173 val res = bash("cp -a " + Bash.string(p1) + " " + Bash.string(p2)) |
173 val res = bash("cp -a " + Bash.string(p1) + " " + Bash.string(p2)) |
174 if (!res.ok) cat_error("Failed to copy " + quote(p1) + " to " + quote(p2), res.err) |
174 if (!res.ok) cat_error("Failed to copy " + quote(p1) + " to " + quote(p2), res.err) |
175 } |
175 } |
176 |
176 |
177 def with_copy_dir[A](dir1: Path, dir2: Path)(body: => A): A = { |
177 def with_copy_dir[A](dir1: Path, dir2: Path)(body: => A): A = { |
178 if (dir2.is_file || dir2.is_dir) error("Directory already exists: " + dir2.absolute) |
178 new_directory(dir2) |
179 else { |
179 try { copy_dir(dir1, dir2, direct = true); body } |
180 try { copy_dir(dir1, dir2); body } |
180 finally { rm_tree(dir2) } |
181 finally { rm_tree(dir2) } |
|
182 } |
|
183 } |
181 } |
184 |
182 |
185 |
183 |
186 object Make_Directory extends Scala.Fun_Strings("make_directory") { |
184 object Make_Directory extends Scala.Fun_Strings("make_directory") { |
187 val here = Scala_Project.here |
185 val here = Scala_Project.here |