diff -r 4a117b57e622 -r 4f1df8d3707b src/Pure/Admin/build_jdk.scala --- 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)