projects
/
pintos-anon
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
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
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
@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}:
Let's take a look at what's inside. Here's the directory structure
that you should see in @file{pintos/src}: