Mention style for references.

diff --git a/doc/standards.texi b/doc/standards.texi
index e7ed5686265f8bd94e89b496b7414f6192c631c3..b95d930d36d13eda918bb7fb516bfb795e97068b 100644 (file)
--- a/doc/standards.texi
+++ b/doc/standards.texi
@@ -41,6 +41,11 @@ them too, especially chapter 5, ``Making the Best Use of C.''  Using a
 different style won't cause actual problems, but it's ugly to see
 gratuitous differences in style from one function to another.
 
 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
 
 @node Conditional Compilation
 @section Conditional Compilation