--- a/src/Pure/Admin/jenkins.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/jenkins.scala Mon Mar 01 22:22:12 2021 +0100
@@ -40,7 +40,7 @@
def download_logs(
- options: Options, job_names: List[String], dir: Path, progress: Progress = new Progress)
+ options: Options, job_names: List[String], dir: Path, progress: Progress = new Progress): Unit =
{
val store = Sessions.store(options)
val infos = job_names.flatMap(build_job_infos)
@@ -96,7 +96,7 @@
}
}
- def download_log(store: Sessions.Store, dir: Path, progress: Progress = new Progress)
+ def download_log(store: Sessions.Store, dir: Path, progress: Progress = new Progress): Unit =
{
val log_dir = dir + Build_Log.log_subdir(date)
val log_path = log_dir + log_filename.xz