equal
deleted
inserted
replaced
150 /** file-system operations **/ |
150 /** file-system operations **/ |
151 |
151 |
152 /* permissions */ |
152 /* permissions */ |
153 |
153 |
154 def chmod(arg: String, path: Path): Unit = |
154 def chmod(arg: String, path: Path): Unit = |
155 bash("chmod " + Bash.string(arg) + " -- " + File.bash_path(path)).check |
155 bash("chmod " + Bash.string(arg) + " " + File.bash_path(path)).check |
156 |
156 |
157 def chown(arg: String, path: Path): Unit = |
157 def chown(arg: String, path: Path): Unit = |
158 bash("chown " + Bash.string(arg) + " -- " + File.bash_path(path)).check |
158 bash("chown " + Bash.string(arg) + " " + File.bash_path(path)).check |
159 |
159 |
160 |
160 |
161 /* directories */ |
161 /* directories */ |
162 |
162 |
163 def mkdirs(path: Path): Unit = |
163 def mkdirs(path: Path): Unit = |