+ // normally we should use clock_gettime(CLOCK_REALTIME) here but this
+ // function is in librt and we don't link with it currently, so use
+ // gettimeofday() instead -- if it turns out that this is really too
+ // imprecise, we should modify configure to check if clock_gettime() is
+ // available and whether it requires -lrt and use it instead
+#if 0