Re: double rounding in xtime_diff()?