+(If the @command{target remote} command fails, then make sure that both
+@command{gdb} and @command{pintos} are running on the same machine by
+running @command{hostname} in each terminal. If the names printed
+differ, then you need to open a new terminal for @command{gdb} on the
+machine running @command{pintos}.)
+