equal
deleted
inserted
replaced
109 """ |
109 """ |
110 |
110 |
111 |
111 |
112 /* extract archive */ |
112 /* extract archive */ |
113 |
113 |
114 private def suppress_name(name: String): Boolean = name.startsWith("._") |
|
115 |
|
116 def extract_archive(dir: Path, archive: Path): JDK_Platform = |
114 def extract_archive(dir: Path, archive: Path): JDK_Platform = |
117 { |
115 { |
118 try { |
116 try { |
119 val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp")) |
117 val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp")) |
120 |
118 |
125 else { |
123 else { |
126 Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check |
124 Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check |
127 } |
125 } |
128 |
126 |
129 val dir_entry = |
127 val dir_entry = |
130 File.read_dir(tmp_dir).filterNot(suppress_name) match { |
128 File.read_dir(tmp_dir) match { |
131 case List(s) => s |
129 case List(s) => s |
132 case _ => error("Archive contains multiple directories") |
130 case _ => error("Archive contains multiple directories") |
133 } |
131 } |
134 |
132 |
135 val jdk_dir = tmp_dir + Path.explode(dir_entry) |
133 val jdk_dir = tmp_dir + Path.explode(dir_entry) |
199 perms.add(PosixFilePermission.GROUP_EXECUTE) |
197 perms.add(PosixFilePermission.GROUP_EXECUTE) |
200 perms.add(PosixFilePermission.OTHERS_EXECUTE) |
198 perms.add(PosixFilePermission.OTHERS_EXECUTE) |
201 } |
199 } |
202 Files.setPosixFilePermissions(path, perms) |
200 Files.setPosixFilePermissions(path, perms) |
203 } |
201 } |
204 |
|
205 File.find_files((component_dir + Path.explode("x86_64-darwin")).file, |
|
206 file => suppress_name(file.getName)).foreach(_.delete) |
|
207 |
202 |
208 progress.echo("Sharing ...") |
203 progress.echo("Sharing ...") |
209 val main_dir :: other_dirs = |
204 val main_dir :: other_dirs = |
210 platforms.map(platform => (component_dir + platform.platform_path).file.toPath) |
205 platforms.map(platform => (component_dir + platform.platform_path).file.toPath) |
211 for { |
206 for { |