Use 9600 bps for Pintos serial, to match the speed used by the loader.
[pintos-anon] / src / lib / user / stdio.h
1 #ifndef __LIB_USER_STDIO_H
2 #define __LIB_USER_STDIO_H
3
4 int hprintf (int, const char *, ...) PRINTF_FORMAT (2, 3);
5 int vhprintf (int, const char *, va_list) PRINTF_FORMAT (2, 0);
6
7 #endif /* lib/user/stdio.h */