more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";

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