Function record_times

src/engine/execnt.cpp:750–763

static void record_times( HANDLE const process, timing_info * const time )
{
    FILETIME creation;
    FILETIME exit;
    FILETIME kernel;
    FILETIME user;
    if ( GetProcessTimes( process, &creation, &exit, &kernel, &user ) )
    {
        time->system = filetime_to_seconds( kernel );
        time->user = filetime_to_seconds( user );
        timestamp_from_filetime( &time->start, &creation );
        timestamp_from_filetime( &time->end, &exit );
    }
}


static char ioBuffer[ IO_BUFFER_SIZE + 1 ];