Rename printk() to printf().

[pintos-anon] / src / devices / disk.h

diff --git a/src/devices/disk.h b/src/devices/disk.h
index d1496827282e06262b0574ccb129f79e17a5f849..9e785e549937079554d063658550bc7372cc8ee0 100644 (file)
--- a/src/devices/disk.h
+++ b/src/devices/disk.h
@@ -11,8 +11,8 @@
    Good enough for disks up to 2 TB. */
 typedef uint32_t disk_sector_t;
 
-/* Format specifier for printk(), e.g.:
-   printk ("sector=%"PRDSNu"\n", sector); */
+/* Format specifier for printf(), e.g.:
+   printf ("sector=%"PRDSNu"\n", sector); */
 #define PRDSNu PRIu32
 
 void disk_init (void);