equal
deleted
inserted
replaced
472 (if (err.isEmpty) "finished" else "ERROR " + err.get) + |
472 (if (err.isEmpty) "finished" else "ERROR " + err.get) + |
473 (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)") |
473 (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)") |
474 log(end_date, msg) |
474 log(end_date, msg) |
475 } |
475 } |
476 |
476 |
477 val log_dir: Path = main_dir + Build_Log.log_subdir(start_date) |
477 val log_dir = Isabelle_System.make_directory(main_dir + Build_Log.log_subdir(start_date)) |
478 |
478 |
479 Isabelle_System.make_directory(log_dir) |
|
480 log(start_date, "started") |
479 log(start_date, "started") |
481 } |
480 } |
482 |
481 |
483 class Task private[Isabelle_Cronjob](name: String, body: => Unit) |
482 class Task private[Isabelle_Cronjob](name: String, body: => Unit) |
484 { |
483 { |