From f3ce70a00e2dd0b7d6640e814e15ef45efabcbf8 Mon Sep 17 00:00:00 2001
From: SimonDold <48084373+SimonDold@users.noreply.github.com>
Date: Mon, 27 Nov 2023 09:33:22 +0100
Subject: [PATCH] [trivial] fix timer precision. (#198)

set precision of the timer to 6 digits.
---
 src/search/utils/timer.cc | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/search/utils/timer.cc b/src/search/utils/timer.cc
index 3267770387..83d0ba6813 100644
--- a/src/search/utils/timer.cc
+++ b/src/search/utils/timer.cc
@@ -1,6 +1,7 @@
 #include "timer.h"
 
 #include <ctime>
+#include <iomanip>
 #include <ostream>
 
 #if OPERATING_SYSTEM == LINUX || OPERATING_SYSTEM == OSX
@@ -110,7 +111,7 @@ Duration Timer::reset() {
 }
 
 ostream &operator<<(ostream &os, const Timer &timer) {
-    os << timer();
+    os << fixed << setprecision(6) << timer();
     return os;
 }