From: Ben Pfaff <blp@cs.stanford.edu>
Date: Thu, 22 Dec 2005 20:49:13 +0000 (+0000)
Subject: Mention that keyboard input does not work with "pintos -v".
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=9087580da55af9d9515c5d7cb73a48a62cf3a36b;p=pintos-anon

Mention that keyboard input does not work with "pintos -v".
---

diff --git a/doc/userprog.texi b/doc/userprog.texi
index c4bd9e1..d401fda 100644
--- a/doc/userprog.texi
+++ b/doc/userprog.texi
@@ -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