diff options
Diffstat (limited to 'context_mirror_bot.ml')
| -rw-r--r-- | context_mirror_bot.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/context_mirror_bot.ml b/context_mirror_bot.ml index 0053126..c2ff29f 100644 --- a/context_mirror_bot.ml +++ b/context_mirror_bot.ml @@ -811,7 +811,7 @@ let () = Git.set_path repo_dir; dispatch_job job.kind; log_info (Printf.sprintf - "mirror bot finished in %.2f ms." + "mirror bot finished in %.2f s." (Unix.gettimeofday () -. t_start)); ;; |