more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
authorwenzelm
Mon Oct 01 12:05:05 2012 +0200 (2012-10-01)
changeset 496732a088cff1e7b
parent 49672 902b24e0ffb4
child 49674 dbadb4d03cbc
more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
src/Pure/General/file.scala
     1.1 --- a/src/Pure/General/file.scala	Mon Oct 01 11:04:30 2012 +0200
     1.2 +++ b/src/Pure/General/file.scala	Mon Oct 01 12:05:05 2012 +0200
     1.3 @@ -105,7 +105,8 @@
     1.4    /* copy */
     1.5  
     1.6    def eq(file1: JFile, file2: JFile): Boolean =
     1.7 -    java.nio.file.Files.isSameFile(file1.toPath, file2.toPath)
     1.8 +    try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) }
     1.9 +    catch { case ERROR(_) => false }
    1.10  
    1.11    def copy(src: JFile, dst: JFile)
    1.12    {