# HG changeset patch
# User wenzelm
# Date 1476364630 -7200
# Node ID dfb63036c4f63ad3fb0c62ced60903444ece3b53
# Parent  f88bae1922c4a26c817046d1ab2235241abf9c4b
tuned signature;
copy_dir using *this* Isabelle_System: note that File.bash_path is already expanded, but no variables are used here;

diff -r f88bae1922c4 -r dfb63036c4f6 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Thu Oct 13 12:13:43 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Thu Oct 13 15:17:10 2016 +0200
@@ -180,7 +180,7 @@
       /* build */
 
       if (multicore_base && !first_build && isabelle_base_log.is_dir)
-        other_isabelle.copy_dir(isabelle_base_log, isabelle_output_log)
+        Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
 
       val build_start = Date.now()
       val res =
@@ -236,7 +236,7 @@
       /* next build */
 
       if (multicore_base && first_build && isabelle_output_log.is_dir)
-        other_isabelle.copy_dir(isabelle_output_log, isabelle_base_log)
+        Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log)
 
       first_build = false
 
diff -r f88bae1922c4 -r dfb63036c4f6 src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Thu Oct 13 12:13:43 2016 +0200
+++ b/src/Pure/Admin/other_isabelle.scala	Thu Oct 13 15:17:10 2016 +0200
@@ -21,9 +21,6 @@
       progress_stdout = progress.echo_if(echo, _),
       progress_stderr = progress.echo_if(echo, _))
 
-  def copy_dir(dir1: Path, dir2: Path): Unit =
-    bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
-
   def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
     bash("bin/isabelle " + cmdline, redirect, echo)
 
diff -r f88bae1922c4 -r dfb63036c4f6 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Oct 13 12:13:43 2016 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Oct 13 15:17:10 2016 +0200
@@ -173,7 +173,7 @@
   }
 
 
-  /* mkdirs */
+  /* directories */
 
   def mkdirs(path: Path): Unit =
     if (!path.is_dir) {
@@ -181,6 +181,9 @@
       if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path)))
     }
 
+  def copy_dir(dir1: Path, dir2: Path): Unit =
+    bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
+
 
   /* tmp files */