Print time with 2 digits after the decimal

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;
 }