Re: [Python-ideas] Improve os.times() resolution