# CONFIG_TIMER_STATS is not set