# CONFIG_RV_MON_SCHED is not set