X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fdevices%2Ftimer.c;h=ecf6c5aacdfee97c6577c8b60912475ef99e4e77;hb=508519ce41b297b341ceb9ad872a457728a90a7b;hp=ec9778321e3339aa2f32bb5496ece5e71a5ea969;hpb=d45c1fe7e69aa616789ffcbff588c60b3fdbf23c;p=pintos-anon

diff --git a/src/devices/timer.c b/src/devices/timer.c
index ec97783..ecf6c5a 100644
--- a/src/devices/timer.c
+++ b/src/devices/timer.c
@@ -66,9 +66,9 @@ timer_sleep (int64_t ticks)
 {
   int64_t start = timer_ticks ();
 
+  ASSERT (intr_get_level () == INTR_ON);
   while (timer_elapsed (start) < ticks) 
-    if (intr_get_level () == INTR_ON)
-      thread_yield ();
+    thread_yield ();
 }
 
 /* Returns MS milliseconds in timer ticks, rounding up. */