# CONFIG_COMPAT_VDSO is not set