Mention that keyboard input does not work with "pintos -v".
[pintos-anon] / doc / userprog.texi
index c4bd9e137bd2c93d4b4c47494d0a581f616d299f..d401fda025f1f98b81ed78a31c743ccbd30bf68e 100644 (file)
@@ -665,7 +665,8 @@ Reads @var{size} bytes from the file open as @var{fd} into
 @var{buffer}.  Returns the number of bytes actually read (0 at end of
 file), or -1 if the file could not be read (due to a condition other
 than end of file).  Fd 0 reads from the keyboard using
-@func{kbd_getc}.
+@func{kbd_getc}.  (Keyboard input will not work if you pass the
+@option{-v} option to @command{pintos}.)
 
 Consider implementing this function in terms of @func{file_read}.
 @end deftypefn