diff options
| author | Philipp Gesang <phg42.2a@gmail.com> | 2014-06-09 12:12:42 +0200 |
|---|---|---|
| committer | Philipp Gesang <phg42.2a@gmail.com> | 2014-06-09 12:12:42 +0200 |
| commit | 5f31770781d14e1f12f3c54e490b4c7e32bab732 (patch) | |
| tree | f49673f47efdfc52d69bc201bd55b0c9a680210d | |
| parent | 75e0e3dab0127f7bad4882b14dbab73a96616495 (diff) | |
| download | context-mirror-bot-5f31770781d14e1f12f3c54e490b4c7e32bab732.tar.gz | |
fix unit for runtime stats
| -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)); ;; |