+You might notice that @command{gdb} tends to show code being executed
+in an order different from the order in the source. That is, the
+current statement jumps around seemingly randomly. This is due to
+GCC's optimizer, which does tend to reorder code. If it bothers you,
+you can turn off optimization by editing
+@file{pintos/src/Make.config}, removing @option{-O3} from the
+@code{CFLAGS} definition.
+
+If you notice other strange behavior while using @command{gdb}, there