X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=blobdiff_plain;f=src%2Flib%2Fkernel%2Fprintf.c;h=c139966f98c358c8804f3c67ce586d49d1286adb;hp=886706c8091223b50ba901a252630803f593e2c3;hb=1873780194ed34a0c8c71a09671938e6e2468afd;hpb=2559f61a41ebfca4f17aae39c89b77a8f1c5c80f

diff --git a/src/lib/kernel/printf.c b/src/lib/kernel/printf.c
index 886706c..c139966 100644
--- a/src/lib/kernel/printf.c
+++ b/src/lib/kernel/printf.c
@@ -1,12 +1,14 @@
 #include <stdarg.h>
 #include <stdio.h>
-
 #include "devices/serial.h"
 #include "devices/vga.h"
 #include "threads/interrupt.h"
 
 static void vprintf_helper (char, void *);
 
+/* The standard vprintf() function,
+   which is like printf() but uses a va_list.
+   Writes its output to both vga display and serial port. */
 int
 vprintf (const char *format, va_list args) 
 {
@@ -29,11 +31,11 @@ vprintf_helper (char c, void *char_cnt_)
   putchar (c);
 }
 
-/* Writes C to the console. */
+/* Writes C to the vga display and serial port. */
 int
 putchar (int c) 
 {
-  serial_outb (c);
+  serial_putc (c);
   vga_putc (c);
   return c;
 }