Add comment.
[pintos-anon] / src / lib / user / printf.c
index d0485f11fd1dfb251c80878925419435a8da80c0..6466e54aaaea8e5f76f46714abf81d3ac5d08c35 100644 (file)
@@ -12,6 +12,9 @@ struct vprintf_aux
     int char_cnt;       /* Total characters written so far. */
   };
 
+/* The standard vprintf() function,
+   which is like printf() but uses a va_list.
+   Writes its output to the STDOUT_FILENO handle. */
 int
 vprintf (const char *format, va_list args) 
 {