src/Pure/General/file.scala
changeset 73318 a45cb064709b
parent 73317 df49ca5da9d0
child 73340 0ffcad1f6130
equal deleted inserted replaced
73317:df49ca5da9d0 73318:a45cb064709b
   292 
   292 
   293 
   293 
   294   /* eq */
   294   /* eq */
   295 
   295 
   296   def eq(file1: JFile, file2: JFile): Boolean =
   296   def eq(file1: JFile, file2: JFile): Boolean =
   297     try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) }
   297     try { Files.isSameFile(file1.toPath, file2.toPath) }
   298     catch { case ERROR(_) => false }
   298     catch { case ERROR(_) => false }
   299 
   299 
   300   def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file)
   300   def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file)
   301 
   301 
   302 
   302