From: Bruno Haible <bruno@clisp.org>
Date: Thu, 6 Mar 2008 17:46:20 +0000 (+0100)
Subject: Talk about "header file", not "header".
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=cff97834265a2dba55ef4b75cdfc329bbcf4b4a8;p=pspp

Talk about "header file", not "header".
---

diff --git a/doc/gnulib.texi b/doc/gnulib.texi
index 16cf858f21..fa4a68ebc7 100644
--- a/doc/gnulib.texi
+++ b/doc/gnulib.texi
@@ -2905,7 +2905,7 @@ specified by ISO C or POSIX are substituted by Gnulib, which portability
 pitfalls are fixed by Gnulib, and which (known) portability problems are
 not worked around by Gnulib.
 
-@nosuchmodulenote header
+@nosuchmodulenote header file
 
 @menu
 * a.out.h::