--- a/src/Pure/Admin/build_jdk.scala Wed Jan 06 14:03:49 2021 +0100
+++ b/src/Pure/Admin/build_jdk.scala Wed Jan 06 14:23:57 2021 +0100
@@ -111,8 +111,6 @@
/* extract archive */
- private def suppress_name(name: String): Boolean = name.startsWith("._")
-
def extract_archive(dir: Path, archive: Path): JDK_Platform =
{
try {
@@ -127,7 +125,7 @@
}
val dir_entry =
- File.read_dir(tmp_dir).filterNot(suppress_name) match {
+ File.read_dir(tmp_dir) match {
case List(s) => s
case _ => error("Archive contains multiple directories")
}
@@ -202,9 +200,6 @@
Files.setPosixFilePermissions(path, perms)
}
- File.find_files((component_dir + Path.explode("x86_64-darwin")).file,
- file => suppress_name(file.getName)).foreach(_.delete)
-
progress.echo("Sharing ...")
val main_dir :: other_dirs =
platforms.map(platform => (component_dir + platform.platform_path).file.toPath)