-(@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}.