tuned signature;
copy_dir using *this* Isabelle_System: note that File.bash_path is already expanded, but no variables are used here;
--- 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
--- 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)
--- 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 */