X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=doc%2Fstandards.texi;h=8e0f0e02bc4a79a4fd1243d2f6d4435fc809ed4e;hb=8abbb333aea445641d967befd3ca477502ea770b;hp=fbd673ae58df14ffb2c24488a892842892013264;hpb=179d174444a023410c175bd2bc0c7f45be0fa508;p=pintos-anon

diff --git a/doc/standards.texi b/doc/standards.texi
index fbd673a..8e0f0e0 100644
--- a/doc/standards.texi
+++ b/doc/standards.texi
@@ -44,7 +44,7 @@ Please limit C source file lines to at most 79 characters long.
 
 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
+@code{[IA32-v3a]}.  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