596 (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r)) |
596 (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r)) |
597 } yield remote_build_history(rev, afp_rev, i, r)))), |
597 } yield remote_build_history(rev, afp_rev, i, r)))), |
598 Logger_Task("build_log_database", |
598 Logger_Task("build_log_database", |
599 logger => |
599 logger => |
600 Build_Log.build_log_database(logger.options, build_log_dirs, |
600 Build_Log.build_log_database(logger.options, build_log_dirs, |
|
601 ml_statistics = true, |
601 snapshot = Some(Isabelle_Devel.build_log_snapshot))), |
602 snapshot = Some(Isabelle_Devel.build_log_snapshot))), |
602 Logger_Task("build_status", |
603 Logger_Task("build_status", |
603 logger => Isabelle_Devel.build_status(logger.options)))))), |
604 logger => Isabelle_Devel.build_status(logger.options)))))), |
604 exit))))) |
605 exit))))) |
605 |
606 |