src/Pure/General/file.scala
changeset 49673 2a088cff1e7b
parent 49610 1b36c6676685
child 50203 00d8ad713e32
equal deleted inserted replaced
49672:902b24e0ffb4 49673:2a088cff1e7b
   103 
   103 
   104 
   104 
   105   /* copy */
   105   /* copy */
   106 
   106 
   107   def eq(file1: JFile, file2: JFile): Boolean =
   107   def eq(file1: JFile, file2: JFile): Boolean =
   108     java.nio.file.Files.isSameFile(file1.toPath, file2.toPath)
   108     try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) }
       
   109     catch { case ERROR(_) => false }
   109 
   110 
   110   def copy(src: JFile, dst: JFile)
   111   def copy(src: JFile, dst: JFile)
   111   {
   112   {
   112     if (!eq(src, dst)) {
   113     if (!eq(src, dst)) {
   113       val in = new FileInputStream(src)
   114       val in = new FileInputStream(src)