X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fintro.texi;h=a74ce8297c91009dad4fa423531a7fee707f613c;hb=2a7028b32e0b34edc8d3d570af1d0d810bea36b4;hp=f5e6fb3239ec8fd76d45c191ec967e5708a1ce97;hpb=73389b59f54bfed8eb0cb370a5ffec1223686a9e;p=pintos-anon

diff --git a/doc/intro.texi b/doc/intro.texi
index f5e6fb3..a74ce82 100644
--- a/doc/intro.texi
+++ b/doc/intro.texi
@@ -17,8 +17,7 @@ systems and software can run under it.  In class we will use the
 @uref{http://bochs.sourceforge.net, , Bochs} and 
 @uref{http://fabrice.bellard.free.fr/qemu/, ,
 qemu} simulators.  Pintos has also been tested with
-@uref{http://www.vmware.com/products/server/gsx_features.html, ,
-VMware GSX Server}.
+@uref{http://www.vmware.com/, , VMware Player}.
 
 These projects are hard.  CS 140 has a reputation of taking a lot of
 time, and deservedly so.  We will do what we can to reduce the workload, such
@@ -35,7 +34,7 @@ projects.
 @menu
 * Getting Started::             
 * Grading::                     
-* License::                     
+* Legal and Ethical Issues::    
 * Acknowledgements::            
 * Trivia::                      
 @end menu
@@ -239,7 +238,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 +254,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 +357,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
@@ -502,12 +502,15 @@ In the end, remember your audience.  Code is written primarily to be
 read by humans.  It has to be acceptable to the compiler too, but the
 compiler doesn't care about how it looks or how well it is written.
 
-@node License
-@section License
+@node Legal and Ethical Issues
+@section Legal and Ethical Issues
 
 Pintos is distributed under a liberal license that allows free use,
 modification, and distribution.  Students and others who work on Pintos
 own the code that they write and may use it for any purpose.
+Pintos comes with NO WARRANTY, not even for MERCHANTABILITY or FITNESS
+FOR A PARTICULAR PURPOSE.
+@xref{License}, for details of the license and lack of warranty.
 
 In the context of Stanford's CS 140 course, please respect the spirit
 and the letter of the honor code by refraining from reading any homework
@@ -516,12 +519,6 @@ other operating system kernels, such as Linux or FreeBSD, is allowed,
 but do not copy code from them literally.  Please cite the code that
 inspired your own in your design documentation.
 
-Pintos comes with NO WARRANTY, not even for MERCHANTABILITY or FITNESS
-FOR A PARTICULAR PURPOSE.
-
-The @file{LICENSE} file at the top level of the Pintos source
-distribution has full details of the license and lack of warranty.
-
 @node Acknowledgements
 @section Acknowledgements