X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fpintos.texi;h=40e702fc7831aa8ab5b1542b4a4e20413f5af474;hb=9f013d0930202eea99c21083b71098a0df64be0d;hp=777b2f45870d603fc2070cd027d2db97822a3cf6;hpb=f415a37905c57f61b444806bf84f5405184452aa;p=pintos-anon

diff --git a/doc/pintos.texi b/doc/pintos.texi
index 777b2f4..40e702f 100644
--- a/doc/pintos.texi
+++ b/doc/pintos.texi
@@ -1,4 +1,5 @@
 \input texinfo                          @c -*- texinfo -*-
+
 @c %**start of header
 @setfilename pintos.info
 @settitle Pintos Projects
@@ -61,9 +62,14 @@
 * Project Documentation::       
 * Debugging Tools::             
 * Development Tools::
+* Installing Pintos::
 * Bibliography::
+* License::
 @end menu
 
+@c institution-local settings
+@include localsettings.texi
+
 @include intro.texi
 @include threads.texi
 @include userprog.texi
@@ -75,6 +81,8 @@
 @include doc.texi
 @include debug.texi
 @include devel.texi
+@include installation.texi
 @include bibliography.texi
+@include license.texi
 
 @bye