X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fintro.texi;h=9f867042c57f2decd83c9a0b75743752bb39cc48;hb=699944803572c46c550a39027c0ebd935b0d61bc;hp=82e45040f3a13268746204e550f7fed732a1e2f4;hpb=19fe94015fe7f89f801652b1dd9d089b01704989;p=pintos-anon

diff --git a/doc/intro.texi b/doc/intro.texi
index 82e4504..9f86704 100644
--- a/doc/intro.texi
+++ b/doc/intro.texi
@@ -224,12 +224,11 @@ The @command{pintos} program offers multiple options for running
 Pintos.  Use @code{pintos help} to see a list of the options.  You can
 select a simulator other than Bochs, although the Leland systems only
 have Bochs installed.  You can start the simulator running a debugger
-(@pxref{Debugging Pintos}).  You can set the amount of memory to give
-the VM.  Finally, you can set up how you want VM output to be
-displayed: use @option{-nv} to turn off the VGA display, @option{-t}
-to use your terminal window as the VGA display instead of opening a
-new window, or @option{-ns} to suppress the serial output to
-@code{stdout}.
+(@pxref{i386-elf-gdb}).  You can set the amount of memory to give the
+VM.  Finally, you can set up how you want VM output to be displayed:
+use @option{-nv} to turn off the VGA display, @option{-t} to use your
+terminal window as the VGA display instead of opening a new window, or
+@option{-ns} to suppress the serial output to @code{stdout}.
 
 The @command{pintos} program offers commands other than @samp{run} and
 @samp{help}, but we won't have any need for them until project 2.