1.1 --- a/src/Pure/General/file.ML	Wed Jul 07 18:17:23 2010 +0200
     1.2 +++ b/src/Pure/General/file.ML	Thu Jul 08 09:36:22 2010 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4    val exists: Path.T -> bool
     1.5    val check: Path.T -> unit
     1.6    val rm: Path.T -> unit
     1.7 +  val rm_tree: Path.T -> unit
     1.8    val mkdir: Path.T -> unit
     1.9    val mkdir_leaf: Path.T -> unit
    1.10    val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
    1.11 @@ -134,6 +135,8 @@
    1.12  
    1.13  val rm = OS.FileSys.remove o platform_path;
    1.14  
    1.15 +fun rm_tree path = system_command ("rm -r " ^ shell_path path);
    1.16 +
    1.17  fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
    1.18  
    1.19  fun mkdir_leaf path = (check (Path.dir path); mkdir path);