# HG changeset patch
# User wenzelm
# Date 1478811298 -3600
# Node ID 43f6c28ff4964fd1a1f586401f21b0b1b573b53f
# Parent  caf62923039baaf5623813318ea0ba99a781c970
clarified File.move: target directory like File.copy;

diff -r caf62923039b -r 43f6c28ff496 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Nov 10 12:14:03 2016 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Nov 10 21:54:58 2016 +0100
@@ -59,8 +59,8 @@
           Build_Release.build_release(base_dir, rev = rev, afp_rev = afp_rev,
             parallel_jobs = 4, remote_mac = "macbroy31", website = Some(new_snapshot))
 
-          if (release_snapshot.is_dir) File.mv(release_snapshot, old_snapshot)
-          File.mv(new_snapshot, release_snapshot)
+          if (release_snapshot.is_dir) File.move(release_snapshot, old_snapshot)
+          File.move(new_snapshot, release_snapshot)
           Isabelle_System.rm_tree(old_snapshot)
         }))
 
@@ -79,7 +79,7 @@
               hg, rev = "build_history_base", fresh = true, build_args = List("HOL"))
         } {
           result.check
-          File.mv(log_path, logger.log_dir + log_path.base)
+          File.move(log_path, logger.log_dir + log_path.base)
         }
       })
 
diff -r caf62923039b -r 43f6c28ff496 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Nov 10 12:14:03 2016 +0100
+++ b/src/Pure/General/file.scala	Thu Nov 10 21:54:58 2016 +0100
@@ -220,13 +220,13 @@
 
   def write_backup(path: Path, text: CharSequence)
   {
-    if (path.is_file) mv(path, path.backup)
+    if (path.is_file) move(path, path.backup)
     write(path, text)
   }
 
   def write_backup2(path: Path, text: CharSequence)
   {
-    if (path.is_file) mv(path, path.backup2)
+    if (path.is_file) move(path, path.backup2)
     write(path, text)
   }
 
@@ -265,8 +265,12 @@
 
   /* move */
 
-  def mv(file1: JFile, file2: JFile): Unit =
-    Files.move(file1.toPath, file2.toPath, StandardCopyOption.REPLACE_EXISTING)
+  def move(src: JFile, dst: JFile)
+  {
+    val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
+    if (!eq(src, target))
+      Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
+  }
 
-  def mv(path1: Path, path2: Path): Unit = mv(path1.file, path2.file)
+  def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file)
 }