3 #include "devices/serial.h"
4 #include "devices/vga.h"
5 #include "threads/interrupt.h"
7 static void vprintf_helper (char, void *);
9 /* The standard vprintf() function,
10 which is like printf() but uses a va_list.
11 Writes its output to both vga display and serial port. */
13 vprintf (const char *format, va_list args)
15 enum intr_level old_level;
18 old_level = intr_disable ();
19 __vprintf (format, args, vprintf_helper, &char_cnt);
20 intr_set_level (old_level);
25 /* Helper function for vprintf(). */
27 vprintf_helper (char c, void *char_cnt_)
29 int *char_cnt = char_cnt_;
34 /* Writes C to the vga display and serial port. */