# 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 = """