X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fpintos.texi;fp=doc%2Fpintos.texi;h=b8e96a0511c535b27ee404c94ef292fabdfad678;hb=21e1ee033ed1c3c41454789ec8c57c7f3a88daf9;hp=1dd83fdc65f1c6317cdefb959430424e40409398;hpb=e08b0009571075c76b710f3051aac1b2f204ae5d;p=pintos-anon

diff --git a/doc/pintos.texi b/doc/pintos.texi
index 1dd83fd..b8e96a0 100644
--- a/doc/pintos.texi
+++ b/doc/pintos.texi
@@ -1,6 +1,6 @@
 \input texinfo                          @c -*- texinfo -*-
 @c %**start of header
-@setfilename projects.info
+@setfilename pintos.info
 @settitle Pintos Projects
 @c %**end of header