Add putbuf().

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

diff --git a/src/lib/stdio.h b/src/lib/stdio.h
index b351dd16a5cf09cf7451dd56b8498a5c9c34aaf8..cf6c49e3ef7841360f6856b2ecb009c88d7bb1e0 100644 (file)
--- a/src/lib/stdio.h
+++ b/src/lib/stdio.h
@@ -19,7 +19,10 @@ int putchar (int);
 int puts (const char *);
 
 /* Nonstandard functions. */
-#ifndef KERNEL
+#ifdef KERNEL
+void putbuf (const char *, size_t);
+#endif
+#ifdef USER
 int hprintf (int, const char *, ...) PRINTF_FORMAT (2, 3);
 int vhprintf (int, const char *, va_list) PRINTF_FORMAT (2, 0);
 #endif