+ printf("available timing options: ");
+#ifdef TIMES
+ printf("TIMES ");
+#endif
+#ifdef TIMEB
+ printf("TIMEB ");
+#endif
+#ifdef USE_TOD
+ printf("USE_TOD ");
+#endif
+#ifdef HZ
+#define as_string(s) (#s)
+ printf("HZ=%g", (double)HZ);
+#endif
+ printf("\n");
+ printf("timing function used: %s%s%s%s%s%s%s\n",
+ (ftime_used ? "ftime" : ""),
+ (ftime_used + times_used > 1 ? "," : ""),
+ (times_used ? "times" : ""),
+ (ftime_used + times_used + gettimeofday_used > 1 ? "," : ""),
+ (gettimeofday_used ? "gettimeofday" : ""),
+ (ftime_used + times_used + gettimeofday_used + getrusage_used > 1 ? "," : ""),
+ (getrusage_used ? "getrusage" : ""));
+