equal
deleted
inserted
replaced
122 /* bash path */ |
122 /* bash path */ |
123 |
123 |
124 def bash_path(path: Path): String = Bash.string(standard_path(path)) |
124 def bash_path(path: Path): String = Bash.string(standard_path(path)) |
125 def bash_path(file: JFile): String = Bash.string(standard_path(file)) |
125 def bash_path(file: JFile): String = Bash.string(standard_path(file)) |
126 |
126 |
|
127 def bash_platform_path(path: Path): String = Bash.string(platform_path(path)) |
|
128 |
127 |
129 |
128 /* directory entries */ |
130 /* directory entries */ |
129 |
131 |
130 def check_dir(path: Path): Path = |
132 def check_dir(path: Path): Path = |
131 if (path.is_dir) path else error("No such directory: " + path) |
133 if (path.is_dir) path else error("No such directory: " + path) |