+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}).