+gratuitous differences in style from one function to another. If your
+code is too ugly, it will cost you points.
+
+Pintos comments sometimes refer to external standards or
+specifications by writing a name inside square brackets, like this:
+@code{[IA32-v3]}. These names refer to the reference names used in
+this documentation (@pxref{References}).
+
+If you remove existing Pintos code, please delete it from your source
+file entirely. Don't just put it into a comment or a conditional
+compilation directive, because that makes the resulting code hard to
+read. We're only going to do a compile in the directory for the current
+project, so you don't need to make sure that the previous projects also
+compile.