# HG changeset patch
# User haftmann
# Date 1278574582 -7200
# Node ID 312fe7201f882f86a6c89abf511a6e42b4d5c86b
# Parent  7bf3ec9e7b0c550855c20faf5a905ba8b03e58b5
rm_tree: remove entire file system trees

diff -r 7bf3ec9e7b0c -r 312fe7201f88 src/Pure/General/file.ML
--- 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);