# CONFIG_PCMCIA is not set