--- a/src/Pure/General/file.ML Wed Jul 07 18:17:23 2010 +0200
+++ b/src/Pure/General/file.ML Thu Jul 08 09:36:22 2010 +0200
@@ -20,6 +20,7 @@
val exists: Path.T -> bool
val check: Path.T -> unit
val rm: Path.T -> unit
+ val rm_tree: Path.T -> unit
val mkdir: Path.T -> unit
val mkdir_leaf: Path.T -> unit
val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
@@ -134,6 +135,8 @@
val rm = OS.FileSys.remove o platform_path;
+fun rm_tree path = system_command ("rm -r " ^ shell_path path);
+
fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
fun mkdir_leaf path = (check (Path.dir path); mkdir path);