58206c6863
Resolves #12515. Use CLOCK_PROCESS_CPUTIME_ID instead of times to get better precision in the value returned by clock.