# CONFIG_PPS_GENERATOR is not set
