X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fprojects.texi;h=f803ac07a8fd99dba5cc9451347e3b26f872c8d0;hb=c20a1ee4a5118c4861b33d39d5d0481eeff59283;hp=90b85e97eb5c6231d9b58c612fb8f2f56dc7618e;hpb=5539377e713d0b7424a15547ca0242518e86ea9b;p=pintos-anon

diff --git a/doc/projects.texi b/doc/projects.texi
index 90b85e9..f803ac0 100644
--- a/doc/projects.texi
+++ b/doc/projects.texi
@@ -1,5 +1,19 @@
+\input texinfo                          @c -*- texinfo -*-
+@c %**start of header
+@setfilename projects.info
+@settitle Pintos Projects
+@c %**end of header
+
+@titlepage
+@title Pintos Projects
+@end titlepage
+
+@contents
+
+@ifnottex
 @node Top, Introduction, (dir), (dir)
 @top Pintos Projects
+@end ifnottex
 
 @menu
 * Introduction::                
@@ -22,3 +36,5 @@
 @include standards.texi
 @include doc.texi
 @include debug.texi
+
+@bye