diff options
| -rw-r--r-- | man/info.texi | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/man/info.texi b/man/info.texi index 24a6c4bbc46..deab84b37af 100644 --- a/man/info.texi +++ b/man/info.texi @@ -1,4 +1,7 @@ -\input texinfo @c -*-texinfo-*- +\input texinfo.tex @c -*-texinfo-*- +@c We must \input texinfo.tex instead of texinfo, otherwise make +@c distcheck in the Texinfo distribution fails, because the texinfo Info +@c file is made first, and texi2dvi must include . first in the path. @comment %**start of header @setfilename info.info @settitle Info |