# HG changeset patch
# User wenzelm
# Date 1512997812 -3600
# Node ID 0da2811afd8702db9d939b936d7a8b0718748d3c
# Parent  dcac4659d482292d98628bad096591fccf836e16
more operations;

diff -r dcac4659d482 -r 0da2811afd87 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sun Dec 10 20:50:09 2017 +0100
+++ b/src/Pure/General/path.scala	Mon Dec 11 14:10:12 2017 +0100
@@ -215,4 +215,7 @@
 
   def absolute_file: JFile = File.absolute(file)
   def canonical_file: JFile = File.canonical(file)
+
+  def absolute: Path = File.path(absolute_file)
+  def canonical: Path = File.path(canonical_file)
 }