# HG changeset patch
# User haftmann
# Date 1277984297 -7200
# Node ID 892f8d00426c64fcb92b46673cc69379c1be4fb7
# Parent  41acc0fa6b6c6dd739d8b58904e3fbfa0377a8be
refined semantics of mkdir_leaf: do not fail if directory already exists

diff -r 41acc0fa6b6c -r 892f8d00426c src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Thu Jul 01 13:32:14 2010 +0200
+++ b/src/Pure/General/file.ML	Thu Jul 01 13:38:17 2010 +0200
@@ -136,7 +136,7 @@
 
 fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
 
-fun mkdir_leaf path = system_command ("mkdir " ^ shell_path path);
+fun mkdir_leaf path = (check (Path.dir path); mkdir path);
 
 fun is_dir path =
   the_default false (try OS.FileSys.isDir (platform_path path));