On 09/25/2017 02:36 PM, Duncan Sands wrote:
+ -- The most recent calls to clock_gettime were more better.were more better -> were better
Yes, we fixed that in a latter commit. :-) https://gcc.gnu.org/git/?p=gcc.git;a=commitdiff;h=2a6c14a68616dfb8d8578bb8692c5e05de4aade3#patch3 -- Pierre-Marie de Rodat
