Header time

このページを編集する際は，編集に関する方針に従ってください．[]

45 /* We may keep statistics about how long which files took to compile.  */
46 static int header_time, body_time;