# CONFIG_INTEL_TDX_HOST is not set