X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Flib%2Fstdio.c;fp=src%2Flib%2Fstdio.c;h=baefaf0eda12774b36b2aa0eddeb6ad0f87ad20b;hb=a7f3ab1350076b71020f6fa859a9b2543a12f6e5;hp=e74d5dd3c5b0bf5d6adb22d97699a5a099e9f69b;hpb=e4f61cdd91a5a7b10abdfa8aba23cc959e2bde8b;p=pintos-anon

diff --git a/src/lib/stdio.c b/src/lib/stdio.c
index e74d5dd..baefaf0 100644
--- a/src/lib/stdio.c
+++ b/src/lib/stdio.c
@@ -74,8 +74,7 @@ snprintf (char *buffer, size_t buf_size, const char *format, ...)
 /* Writes formatted output to the console.
    In the kernel, the console is both the video display and first
    serial port.
-   In userspace, the console is file descriptor 1.
-*/
+   In userspace, the console is file descriptor 1. */
 int
 printf (const char *format, ...) 
 {