Add installation chapter to manual. Remove now-redundant files from

[pintos-anon] / doc / pintos.texi

diff --git a/doc/pintos.texi b/doc/pintos.texi
index 777b2f45870d603fc2070cd027d2db97822a3cf6..ac1612717747f49d58407f8d581af178c931d1c0 100644 (file)
--- a/doc/pintos.texi
+++ b/doc/pintos.texi
@@ -61,7 +61,9 @@
 * Project Documentation::       
 * Debugging Tools::             
 * Development Tools::
+* Installing Pintos::
 * Bibliography::
+* License::
 @end menu
 
 @include intro.texi
@@ -75,6 +77,8 @@
 @include doc.texi
 @include debug.texi
 @include devel.texi
+@include installation.texi
 @include bibliography.texi
+@include license.texi
 
 @bye