equal
deleted
inserted
replaced
56 else (); |
56 else (); |
57 |
57 |
58 |
58 |
59 (* directory operations *) |
59 (* directory operations *) |
60 |
60 |
61 fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path); |
61 fun mkdirs path = |
|
62 if #rc (Bash.process ("mkdir -p " ^ File.shell_path path)) <> 0 then |
|
63 error ("Failed to create directory: " ^ Path.print path) |
|
64 else (); |
62 |
65 |
63 fun mkdir path = |
66 fun mkdir path = |
64 if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path); |
67 if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path); |
65 |
68 |
66 fun copy_dir src dst = |
69 fun copy_dir src dst = |