diff -r 7188967253e5 -r 836898197296 src/Pure/General/url.scala --- a/src/Pure/General/url.scala Fri Jun 30 14:17:48 2017 +0200 +++ b/src/Pure/General/url.scala Fri Jun 30 14:19:37 2017 +0200 @@ -49,7 +49,7 @@ /* file URIs */ - def print_file(file: JFile): String = file.toPath.toAbsolutePath.toUri.normalize.toString + def print_file(file: JFile): String = File.absolute(file).toPath.toUri.toString def print_file_name(name: String): String = print_file(new JFile(name)) def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile @@ -61,6 +61,6 @@ false } - def canonical_file(uri: String): JFile = parse_file(uri).getCanonicalFile + def canonical_file(uri: String): JFile = File.canonical(parse_file(uri)) def canonical_file_name(uri: String): String = canonical_file(uri).getPath }