Make interrupt.h names more regular.
[pintos-anon] / src / lib / debug.c
index 3d9a9b1e28f159f1d1dc0a82d7e117c6a6f02bac..9fbf20656c66833b2dee6948c5ce167f6cb297aa 100644 (file)
@@ -53,7 +53,7 @@ debug_message (const char *file, int line, const char *function,
     {
       va_list args;
 
-      enum if_level old_level = intr_disable ();
+      enum intr_level old_level = intr_disable ();
       printk ("%s:%d: %s(): ", file, line, function);
       va_start (args, message);
       vprintk (message, args);