# HG changeset patch
# User wenzelm
# Date 1478770901 -3600
# Node ID 84e1655ad7778ecdeae6c19cd3b35c06944d51df
# Parent  9d643c4e940386ab0651a8f2622ce6db142e45bd
proper cleanup;

diff -r 9d643c4e9403 -r 84e1655ad777 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Nov 10 10:35:34 2016 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Nov 10 10:41:41 2016 +0100
@@ -79,7 +79,7 @@
               hg, rev = "build_history_base", fresh = true, build_args = List("HOL"))
         } {
           result.check
-          File.copy(log_path, logger.log_dir + log_path.base)
+          File.mv(log_path, logger.log_dir + log_path.base)
         }
       })