# 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)