-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{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}.
+Pintos. Specify these options on the command line @emph{before} the
+@option{run} command. 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{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{-v} 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{-s} to suppress the serial output to
+@code{stdout}.