X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fintro.texi;h=5372f74bb6a266d2787ec1c45264823996bd2ae7;hb=919347c164606c3f1544b2e8bd62f505aeda80a1;hp=8e935bb5a57d9456546f7d7112215972d30ca9c3;hpb=bffccc54acc0560186b8c38bc4a66897de5158eb;p=pintos-anon

diff --git a/doc/intro.texi b/doc/intro.texi
index 8e935bb..5372f74 100644
--- a/doc/intro.texi
+++ b/doc/intro.texi
@@ -68,11 +68,8 @@ environment.
 Now you can extract the source for Pintos into a directory named
 @file{pintos/src}, by executing
 @example
-zcat @value{localpintostarpath} | tar x
+git clone @value{gitrepo}
 @end example
-Alternatively, fetch
-@uref{@value{localpintoshttppath}}
-and extract it in a similar way.
 
 Let's take a look at what's inside.  Here's the directory structure
 that you should see in @file{pintos/src}: