equal
deleted
inserted
replaced
49 dir + Path.explode("contrib") + Path.explode(name) |
49 dir + Path.explode("contrib") + Path.explode(name) |
50 |
50 |
51 def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = { |
51 def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = { |
52 val name = Archive.get_name(archive.file_name) |
52 val name = Archive.get_name(archive.file_name) |
53 progress.echo("Unpacking " + name) |
53 progress.echo("Unpacking " + name) |
54 Isabelle_System.extract(archive, dir) |
54 Isabelle_System.bash( |
|
55 "tar -C " + File.bash_path(dir) + " -x -z -f " + File.bash_path(archive)).check |
55 name |
56 name |
56 } |
57 } |
57 |
58 |
58 def resolve(base_dir: Path, names: List[String], |
59 def resolve(base_dir: Path, names: List[String], |
59 target_dir: Option[Path] = None, |
60 target_dir: Option[Path] = None, |