src/Pure/General/file.ML

--- a/src/Pure/General/file.ML	Wed Jun 30 11:39:10 2010 +0200
+++ b/src/Pure/General/file.ML	Wed Jun 30 12:20:45 2010 +0200
@@ -21,6 +21,7 @@
   val check: Path.T -> unit
   val rm: Path.T -> unit
   val mkdir: Path.T -> unit
+  val mkdir_leaf: Path.T -> unit
   val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
   val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
   val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
@@ -135,6 +136,8 @@
 
 fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
 
+fun mkdir_leaf path = system_command ("mkdir " ^ shell_path path);
+
 fun is_dir path =
   the_default false (try OS.FileSys.isDir (platform_path path));