Rename printk() to printf().
[pintos-anon] / src / devices / timer.c
index 85bc3ee33d3345fa519f6d3cbd80c1011aee01e1..1706201f4ea8590b54a9bc58792667128bb23cf7 100644 (file)
@@ -1,5 +1,5 @@
-#include "timer.h"
-#include "lib/debug.h"
+#include "devices/timer.h"
+#include <debug.h>
 #include "threads/interrupt.h"
 #include "threads/io.h"