more operations;
authorwenzelm
Mon Dec 11 14:10:12 2017 +0100 (17 months ago)
changeset 671810da2811afd87
parent 67180 dcac4659d482
child 67182 bdc03e20fce3
more operations;
src/Pure/General/path.scala
     1.1 --- a/src/Pure/General/path.scala	Sun Dec 10 20:50:09 2017 +0100
     1.2 +++ b/src/Pure/General/path.scala	Mon Dec 11 14:10:12 2017 +0100
     1.3 @@ -215,4 +215,7 @@
     1.4  
     1.5    def absolute_file: JFile = File.absolute(file)
     1.6    def canonical_file: JFile = File.canonical(file)
     1.7 +
     1.8 +  def absolute: Path = File.path(absolute_file)
     1.9 +  def canonical: Path = File.path(canonical_file)
    1.10  }