Rename printk() to printf().

[pintos-anon] / src / lib / stdlib.h

diff --git a/src/lib/stdlib.h b/src/lib/stdlib.h
new file mode 100644 (file)
index 0000000..0a8abcb
--- /dev/null
+++ b/src/lib/stdlib.h
@@ -0,0 +1,8 @@
+#ifndef LIB_STDLIB_H
+#define LIB_STDLIB_H
+
+#include "stddef.h"
+
+int atoi (const char *);
+
+#endif /* lib/stdlib.h */