Fix typos.

[pintos-anon] / doc / intro.texi

diff --git a/doc/intro.texi b/doc/intro.texi
index f5e6fb3239ec8fd76d45c191ec967e5708a1ce97..c4846908c14bbb9db5db6f10d5192d3d66ab8a3c 100644 (file)
--- a/doc/intro.texi
+++ b/doc/intro.texi
@@ -239,7 +239,8 @@ read.  However, you've probably noticed by now that the same text was
 displayed in the terminal you used to run @command{pintos}.  This is
 because Pintos sends all output both to the VGA display and to the first
 serial port, and by default the serial port is connected to Bochs's
-@code{stdout}.  You can log this output to a file by redirecting at the
+@code{stdin} and @code{stdout}.  You can log serial output to a file by
+redirecting at the
 command line, e.g.@: @code{pintos run alarm-multiple > logfile}.
 
 The @command{pintos} program offers several options for configuring the
@@ -254,8 +255,8 @@ with a debugger (@pxref{GDB}).  You can set the amount of memory to give
 the VM.  Finally, you can select how you want VM output to be displayed:
 use @option{-v} to turn off the VGA display, @option{-t} to use your
 terminal window as the VGA display instead of opening a new window
-(Bochs only), or @option{-s} to suppress the serial output to
-@code{stdout}.
+(Bochs only), or @option{-s} to suppress serial input from @code{stdin}
+and output to @code{stdout}.
 
 The Pintos kernel has commands and options other than @command{run}.
 These are not very interesting for now, but you can see a list of them
@@ -357,7 +358,7 @@ specifying @option{VERBOSE=1} on the @command{make} command line, as in
 @code{make check VERBOSE=1}.  You can also provide arbitrary options to the
 @command{pintos} run by the tests with @option{PINTOSOPTS='@dots{}'},
 e.g.@: @code{make check PINTOSOPTS='-j 1'} to select a jitter value of 1
-(@pxref{Debugging Versus Testing}).
+(@pxref{Debugging versus Testing}).
 
 All of the tests and related files are in @file{pintos/src/tests}.
 Before we test your submission, we will replace the contents of that