# HG changeset patch
# User wenzelm
# Date 1349085905 -7200
# Node ID 2a088cff1e7b60c072fa1a589df855c5882493c1
# Parent  902b24e0ffb4818885aee42c83f862912f5c7868
more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";

diff -r 902b24e0ffb4 -r 2a088cff1e7b src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Oct 01 11:04:30 2012 +0200
+++ b/src/Pure/General/file.scala	Mon Oct 01 12:05:05 2012 +0200
@@ -105,7 +105,8 @@
   /* copy */
 
   def eq(file1: JFile, file2: JFile): Boolean =
-    java.nio.file.Files.isSameFile(file1.toPath, file2.toPath)
+    try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) }
+    catch { case ERROR(_) => false }
 
   def copy(src: JFile, dst: JFile)
   {