equal
deleted
inserted
replaced
34 |
34 |
35 def unpack(dir: Path, archive: Path, progress: Progress = No_Progress): String = |
35 def unpack(dir: Path, archive: Path, progress: Progress = No_Progress): String = |
36 { |
36 { |
37 val name = Archive.get_name(archive.file_name) |
37 val name = Archive.get_name(archive.file_name) |
38 progress.echo("Unpacking " + name) |
38 progress.echo("Unpacking " + name) |
39 Isabelle_System.gnutar( |
39 Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check |
40 "-C " + File.bash_path(dir) + " -xzf " + File.bash_path(archive.absolute)).check |
|
41 name |
40 name |
42 } |
41 } |
43 |
42 |
44 def resolve(base_dir: Path, names: List[String], |
43 def resolve(base_dir: Path, names: List[String], |
45 target_dir: Option[Path] = None, |
44 target_dir: Option[Path] = None, |