# CONFIG_TICK_DIVIDER is not set
