# CONFIG_PPS_GENERATOR_DUMMY is not set
