Update docs.

[pintos-anon] / doc / intro.texi

diff --git a/doc/intro.texi b/doc/intro.texi
index 94a1bd6e42c8e3f8155852fe7cde345b547ed41b..81b54fb5e11057721d5617675bf12168ad89896c 100644 (file)
--- a/doc/intro.texi
+++ b/doc/intro.texi
@@ -1,4 +1,4 @@
-@node Introduction, Project 1--Threads, Top, Top
+@node Introduction, Pintos Tour, Top, Top
 @chapter Introduction
 
 Welcome to Pintos.  Pintos is a simple operating system framework for