/* Disable the 32 kHz clock output to other peripherals.  */
void RTCClockOutputPeripheralsDisable(void)
/* Disable the 32 kHz clock output to other peripherals.  */
void RTCClockOutputPeripheralsDisable(void)
{
    xHWREG(RTC_CR) |= RTC_CR_CLKO;
}