equal
deleted
inserted
replaced
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 file1.getCanonicalPath == file2.getCanonicalPath // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7 |
108 java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) |
109 |
109 |
110 def copy(src: JFile, dst: JFile) |
110 def copy(src: JFile, dst: JFile) |
111 { |
111 { |
112 if (!eq(src, dst)) { |
112 if (!eq(src, dst)) { |
113 val in = new FileInputStream(src) |
113 val in = new FileInputStream(src) |