Eliminate race condition in timer_print_stats() found by Sorav's

[pintos-anon] / src / devices / timer.c

diff --git a/src/devices/timer.c b/src/devices/timer.c
index 24eede0e247e8c1f389be38f129dda96d81ffb80..c8c41d55cf412948eb71a04b52c748f0c554465d 100644 (file)
--- a/src/devices/timer.c
+++ b/src/devices/timer.c
@@ -123,7 +123,7 @@ timer_nsleep (int64_t ns)
 void
 timer_print_stats (void) 
 {
-  printf ("Timer: %"PRId64" ticks\n", ticks);
+  printf ("Timer: %"PRId64" ticks\n", timer_ticks ());
 }
 \f
 /* Timer interrupt handler. */