+ } else {
+ if (!quiet) {
+ static const char* const units[] = {
+ "s" /* PRECISION_SECONDS */,
+ "ms" /* PRECISION_MILLI */,
+ "us" /* PRECISION_MICRO */,
+ "ns" /* PRECISION_NANO */,
+ };
+ infostream << m_name << " took "
+ << dtime << units[m_precision]
+ << std::endl;
+ }