From 6bed3ac69751374dbbc221a13130010394f3fbf7 Mon Sep 17 00:00:00 2001
From: Patrick Pelissier <Patrick.Pelissier@gmail.com>
Date: Sat, 8 Apr 2023 11:25:59 +0200
Subject: [PATCH] Print time with 2 digits after the decimal

---
 bench/common.h | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/bench/common.h b/bench/common.h
index 6895ed18..4a7c1242 100644
--- a/bench/common.h
+++ b/bench/common.h
@@ -55,7 +55,7 @@
 // Number of elements of a table
 #define numberof(x) (sizeof(x)/sizeof(x[0]))
 
-/* Get the current CPU time. */
+/* Get the current CPU time in microsecond. */
 #if defined(_WIN32)
 /* WINDOWS variant */
 static inline unsigned long long
@@ -119,9 +119,8 @@ test_function(const char *str, size_t n, void (*func)(size_t))
   (*func)(n);
   end = cputime();
   result = (double)(end-start) / 1000.0;
-  end = (end - start) / 1000U;
   if (str != NULL) {
-    printf ("%20.20s time %lu ms for n = %lu [r=%lu]\n", str, (unsigned long) end, (unsigned long) n, g_result);
+    printf ("%20.20s time %.2f ms for n = %lu [r=%lu]\n", str, result, (unsigned long) n, g_result);
   }
   return result;
 }