# CONFIG_IBMVMC is not set