equal
deleted
inserted
replaced
255 |
255 |
256 |
256 |
257 /* mkdirs */ |
257 /* mkdirs */ |
258 |
258 |
259 def mkdirs(path: Path): Unit = |
259 def mkdirs(path: Path): Unit = |
260 if (bash("mkdir -p " + shell_path(path)).rc != 0) |
260 if (path.is_dir || bash("mkdir -p " + shell_path(path)).rc == 0) () |
261 error("Failed to create directory: " + quote(platform_path(path))) |
261 else error("Failed to create directory: " + quote(platform_path(path))) |
262 |
262 |
263 |
263 |
264 |
264 |
265 /** external processes **/ |
265 /** external processes **/ |
266 |
266 |