Switch docs to use Git instead of CVS by default

[pintos-anon] / doc / intro.texi

diff --git a/doc/intro.texi b/doc/intro.texi
index 8e935bb5a57d9456546f7d7112215972d30ca9c3..5372f74bb6a266d2787ec1c45264823996bd2ae7 100644 (file)
--- 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}: