/* Enable the 32 kHz clock output to other peripherals.  */
void RTCClockOutputPeripheralsEnable(void)
/* Enable the 32 kHz clock output to other peripherals.  */
void RTCClockOutputPeripheralsEnable(void)
{
    xHWREG(RTC_CR) &= ~RTC_CR_CLKO;
}