/* 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, ...)
{