equal
deleted
inserted
replaced
116 if (other_path.startsWith(base_path)) |
116 if (other_path.startsWith(base_path)) |
117 Some(path(base_path.relativize(other_path).toFile)) |
117 Some(path(base_path.relativize(other_path).toFile)) |
118 else None |
118 else None |
119 } |
119 } |
120 |
120 |
121 def rebase_path(base: Path, other: Path): Option[Path] = |
|
122 relative_path(base, other).map(base + _) |
|
123 |
|
124 |
121 |
125 /* bash path */ |
122 /* bash path */ |
126 |
123 |
127 def bash_path(path: Path): String = Bash.string(standard_path(path)) |
124 def bash_path(path: Path): String = Bash.string(standard_path(path)) |
128 def bash_path(file: JFile): String = Bash.string(standard_path(file)) |
125 def bash_path(file: JFile): String = Bash.string(standard_path(file)) |