equal
deleted
inserted
replaced
97 } |
97 } |
98 |
98 |
99 def download_log(store: Sessions.Store, dir: Path, progress: Progress = new Progress) |
99 def download_log(store: Sessions.Store, dir: Path, progress: Progress = new Progress) |
100 { |
100 { |
101 val log_dir = dir + Build_Log.log_subdir(date) |
101 val log_dir = dir + Build_Log.log_subdir(date) |
102 val log_path = log_dir + log_filename.ext("xz") |
102 val log_path = log_dir + log_filename.xz |
103 |
103 |
104 if (!log_path.is_file) { |
104 if (!log_path.is_file) { |
105 progress.echo(log_path.expand.implode) |
105 progress.echo(log_path.expand.implode) |
106 Isabelle_System.make_directory(log_dir) |
106 Isabelle_System.make_directory(log_dir) |
107 |
107 |