/* * The real-time timer, interrupting hz times per second. */