changeset 65833 | 95fd3b9888e6 |
parent 65559 | 7ff7781913a4 |
child 65999 | ee4cf96a9406 |
--- a/src/Pure/General/path.scala Sun May 14 20:16:13 2017 +0200 +++ b/src/Pure/General/path.scala Sun May 14 20:22:54 2017 +0200 @@ -211,4 +211,6 @@ def file: JFile = File.platform_file(this) def is_file: Boolean = file.isFile def is_dir: Boolean = file.isDirectory + + def canonical_file: JFile = file.getCanonicalFile }