# HG changeset patch
# User wenzelm
# Date 1444399634 -7200
# Node ID 17944b500166669a950f75c70caee4c138d5cfcb
# Parent  e78e6b059ba3c7e1e53732d94dd1a2c36e1c2c09
clarified, according to Isabelle_System.copy_file in ML;

diff -r e78e6b059ba3 -r 17944b500166 src/Pure/General/file.scala
--- 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