equal
deleted
inserted
replaced
246 { |
246 { |
247 val (prfx, s) = split_path |
247 val (prfx, s) = split_path |
248 prfx + Path.basic(s + "~~") |
248 prfx + Path.basic(s + "~~") |
249 } |
249 } |
250 |
250 |
251 def platform_exe: Path = |
251 def exe: Path = ext("exe") |
252 if (Platform.is_windows) ext("exe") else this |
252 def platform_exe: Path = if (Platform.is_windows) exe else this |
253 |
253 |
254 private val Ext = new Regex("(.*)\\.([^.]*)") |
254 private val Ext = new Regex("(.*)\\.([^.]*)") |
255 |
255 |
256 def split_ext: (Path, String) = |
256 def split_ext: (Path, String) = |
257 { |
257 { |