From 9f6a072593f75a3ef8337156940d7cf1c090966d Mon Sep 17 00:00:00 2001 From: Ben Pfaff Date: Wed, 1 Dec 2004 19:40:12 +0000 Subject: [PATCH] Fix Info file name. --- doc/pintos.texi | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.30.2