# CONFIG_IPX_INTERN is not set