equal
deleted
inserted
replaced
216 Isabelle_System.with_tmp_dir("mercurial")(tmp_dir => |
216 Isabelle_System.with_tmp_dir("mercurial")(tmp_dir => |
217 { |
217 { |
218 val archive = |
218 val archive = |
219 if (Url.is_wellformed(mercurial_source)) { |
219 if (Url.is_wellformed(mercurial_source)) { |
220 val archive = tmp_dir + Path.basic("mercurial.tar.gz") |
220 val archive = tmp_dir + Path.basic("mercurial.tar.gz") |
221 Bytes.write(archive, Url.read_bytes(Url(mercurial_source))) |
221 Isabelle_System.download(mercurial_source, archive) |
222 archive |
222 archive |
223 } |
223 } |
224 else Path.explode(mercurial_source) |
224 else Path.explode(mercurial_source) |
225 |
225 |
226 Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check |
226 Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check |