X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fstandards.texi;h=b95d930d36d13eda918bb7fb516bfb795e97068b;hb=4600899b8430f10a10e13761829bff41bc5ca902;hp=e7ed5686265f8bd94e89b496b7414f6192c631c3;hpb=cb23eeb534a85547c427b695b6838e5792e31ddb;p=pintos-anon

diff --git a/doc/standards.texi b/doc/standards.texi
index e7ed568..b95d930 100644
--- 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.
 
+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