equal
deleted
inserted
replaced
33 |
33 |
34 def standard_path(p: Path, dir: Boolean = false): Source = |
34 def standard_path(p: Path, dir: Boolean = false): Source = |
35 string(File.standard_path(p) + (if (dir) "/" else "")) |
35 string(File.standard_path(p) + (if (dir) "/" else "")) |
36 |
36 |
37 def platform_path(p: Path, dir: Boolean = false): Source = |
37 def platform_path(p: Path, dir: Boolean = false): Source = |
38 string(File.platform_path(p) + (if (dir) File.platform_path(Path.root) else "")) |
38 string(File.platform_path(p) + (if (dir) "/" else "")) |
39 } |
39 } |