# HG changeset patch # User wenzelm # Date 1348751066 -7200 # Node ID 1b36c66766853b832663a6ca9378a4e0fede9417 # Parent 89e10ed7668bbc58502e065da654160c65196006 physical File.eq in conformance to Isabelle/ML; diff -r 89e10ed7668b -r 1b36c6676685 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Thu Sep 27 14:52:50 2012 +0200 +++ b/src/Pure/General/file.scala Thu Sep 27 15:04:26 2012 +0200 @@ -105,7 +105,7 @@ /* copy */ def eq(file1: JFile, file2: JFile): Boolean = - file1.getCanonicalPath == file2.getCanonicalPath // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7 + java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) def copy(src: JFile, dst: JFile) {