# HG changeset patch # User wenzelm # Date 1614451364 -3600 # Node ID a45cb064709b0220145ca4fa03839ea5036c5252 # Parent df49ca5da9d037ef99b223624386230f14a114ea tuned; diff -r df49ca5da9d0 -r a45cb064709b src/Pure/General/file.scala --- a/src/Pure/General/file.scala Sat Feb 27 18:04:29 2021 +0100 +++ b/src/Pure/General/file.scala Sat Feb 27 19:42:44 2021 +0100 @@ -294,7 +294,7 @@ /* eq */ def eq(file1: JFile, file2: JFile): Boolean = - try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) } + try { Files.isSameFile(file1.toPath, file2.toPath) } catch { case ERROR(_) => false } def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file)