# CONFIG_NO_HZ_FULL is not set