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

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}: