author | wenzelm |
Fri, 09 Oct 2015 16:07:14 +0200 | |
changeset 61371 | 17944b500166 |
parent 61370 | e78e6b059ba3 |
child 61372 | cf40b6b1de54 |
--- a/src/Pure/General/file.scala Fri Oct 09 01:44:29 2015 +0200 +++ b/src/Pure/General/file.scala Fri Oct 09 16:07:14 2015 +0200 @@ -219,10 +219,12 @@ def copy(src: JFile, dst: JFile) { - if (!eq(src, dst)) { + val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst + + if (!eq(src, target)) { val in = new FileInputStream(src) try { - val out = new FileOutputStream(dst) + val out = new FileOutputStream(target) try { val buf = new Array[Byte](65536) var m = 0