else
#endif /* HAVE_SGI_SAVER_EXTENSION */
/* Just some random event. Never mind */
break;
}
if (reset_timers_for_current_event_loop) {