Make interrupt.h names more regular.

[pintos-anon] / src / lib / lib.c

diff --git a/src/lib/lib.c b/src/lib/lib.c
index 6e676cd1a6b1c9e04e356d08b83c23d18910c63c..c88c4a6b40f5c2b97dfb8485cc462f5e92edc1b2 100644 (file)
--- a/src/lib/lib.c
+++ b/src/lib/lib.c
@@ -245,7 +245,7 @@ vprintk_helper (char ch, void *aux UNUSED)
 void
 vprintk (const char *format, va_list args) 
 {
-  enum if_level old_level = intr_disable ();
+  enum intr_level old_level = intr_disable ();
   vprintf_core (format, args, vprintk_helper, NULL);
   intr_set_level (old_level);
 }