author | wenzelm |
Sat, 27 Feb 2021 19:42:44 +0100 | |
changeset 73318 | a45cb064709b |
parent 73317 | df49ca5da9d0 |
child 73319 | a7d9edd2e63b |
--- 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)