MAX_TICKADJ_SCALED  204 kernel/time/ntp.c 			tick_length += MAX_TICKADJ_SCALED;
MAX_TICKADJ_SCALED  207 kernel/time/ntp.c 			tick_length -= MAX_TICKADJ_SCALED;