| changeset 37668 | 892f8d00426c |
| parent 37651 | 62fc16341922 |
| child 37739 | 312fe7201f88 |
--- 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));