different style won't cause actual problems, but it's ugly to see
gratuitous differences in style from one function to another.
+Pintos comments sometimes refer to outside 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}).
+
@node Conditional Compilation
@section Conditional Compilation