# HG changeset patch
# User wenzelm
# Date 1485085579 -3600
# Node ID 8d30727cd56f7cab1954392dd57cb16046eeaefe
# Parent  3b4e5fad4dc23c599d8da23eaedcd02c2b78f388
tuned;

diff -r 3b4e5fad4dc2 -r 8d30727cd56f src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Sun Jan 22 00:30:10 2017 +0100
+++ b/src/Pure/Admin/build_jdk.scala	Sun Jan 22 12:46:19 2017 +0100
@@ -118,8 +118,7 @@
 
       val platform_dir = dir + Path.explode(platform.name)
       if (platform_dir.is_dir) error("Directory already exists: " + platform_dir)
-      Isabelle_System.bash(
-        "mv " + File.bash_path(jdk_dir) + " " + File.bash_path(platform_dir)).check
+      File.move(jdk_dir, platform_dir)
 
       (version, platform)
     }
@@ -163,11 +162,8 @@
         File.write(component_dir + Path.explode("etc/settings"), settings)
         File.write(component_dir + Path.explode("README"), readme(version))
 
-        for ((_, platform) <- extracted) {
-          Isabelle_System.bash("mv " +
-            File.bash_path(dir + Path.explode(platform.name)) + " " +
-            File.bash_path(component_dir)).check
-        }
+        for ((_, platform) <- extracted)
+          File.move(dir + Path.explode(platform.name), component_dir)
 
         Isabelle_System.bash(cwd = component_dir.file,
           script = """