# CONFIG_OPROFILE is not set