X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fintro.texi;h=c4846908c14bbb9db5db6f10d5192d3d66ab8a3c;hb=7641b4a058aedefcf6430000ec7742881f9e2a9f;hp=6541cf1b903f5a46f141da68af72a7f68310da90;hpb=837e5b7fb902bd749106309ef76a5276c73ca34c;p=pintos-anon

diff --git a/doc/intro.texi b/doc/intro.texi
index 6541cf1..c484690 100644
--- a/doc/intro.texi
+++ b/doc/intro.texi
@@ -358,7 +358,7 @@ specifying @option{VERBOSE=1} on the @command{make} command line, as in
 @code{make check VERBOSE=1}.  You can also provide arbitrary options to the
 @command{pintos} run by the tests with @option{PINTOSOPTS='@dots{}'},
 e.g.@: @code{make check PINTOSOPTS='-j 1'} to select a jitter value of 1
-(@pxref{Debugging Versus Testing}).
+(@pxref{Debugging versus Testing}).
 
 All of the tests and related files are in @file{pintos/src/tests}.
 Before we test your submission, we will replace the contents of that