equal
deleted
inserted
replaced
92 private def suppress_name(name: String): Boolean = name.startsWith("._") |
92 private def suppress_name(name: String): Boolean = name.startsWith("._") |
93 |
93 |
94 def extract_archive(dir: Path, archive: Path): (String, JDK_Platform) = |
94 def extract_archive(dir: Path, archive: Path): (String, JDK_Platform) = |
95 { |
95 { |
96 try { |
96 try { |
97 val tmp_dir = dir + Path.explode("tmp") |
97 val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp")) |
98 Isabelle_System.make_directory(tmp_dir) |
|
99 |
98 |
100 if (archive.get_ext == "zip") { |
99 if (archive.get_ext == "zip") { |
101 Isabelle_System.bash( |
100 Isabelle_System.bash( |
102 "unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check |
101 "unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check |
103 } |
102 } |