Make interrupt.h names more regular.

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

diff --git a/src/devices/timer.c b/src/devices/timer.c
index df387367e72b3b531dc094ad585b263729c31807..4271c7354a86b6bf153045cad2666c5e2855faa5 100644 (file)
--- a/src/devices/timer.c
+++ b/src/devices/timer.c
@@ -30,13 +30,13 @@ timer_init (void)
   outb (0x40, count & 0xff);
   outb (0x40, count >> 8);
 
-  intr_register (0x20, 0, IF_OFF, irq20_timer, "8254 Timer");
+  intr_register (0x20, 0, INTR_OFF, irq20_timer, "8254 Timer");
 }
 
 int64_t
 timer_ticks (void) 
 {
-  enum if_level old_level = intr_disable ();
+  enum intr_level old_level = intr_disable ();
   int64_t t = ticks;
   intr_set_level (old_level);
   return t;