# CONFIG_DEBUG_HOTPLUG_CPU0 is not set