[Python-Dev] time.clock_info() field names