src/Pure/General/path.scala
changeset 75273 f1c6e778e412
parent 75230 bbbee54b1198
child 75312 e641ac92b489
equal deleted inserted replaced
75272:3ee89eaa0b55 75273:f1c6e778e412
   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   {