diff options
| author |  Teemu Likonen <tlikonen@iki.fi> | 2008-12-29 10:03:09 +0200 |
|---|---|---|
| committer |  Junio C Hamano <gitster@pobox.com> | 2008-12-29 00:40:10 -0800 |
| commit | 9c6c304d6a01b72d7ce20722b80ca62e01fe8356 (patch) | |
| tree | 4afcf9a56e11ccfb4d308b130f4a06fc360e2691 /grep.h | |
| parent | Fix the building of user-manual.texi and gitman.texi documents (diff) | |
| download | tgif-9c6c304d6a01b72d7ce20722b80ca62e01fe8356.tar.xz | |
Fix the building of gitman.info document
"makeinfo" failed to generate gitman.info from gitman.texi input file
because the combined manual page file contains several nodes with the
same name (DESCRIPTION, OPTIONS, SEE ALSO etc.). An Info document should
contain unique node names.
This patch creates a simple (read: ugly) work-around by suppressing the
validation of the final Info file. Jumping to nodes in the Info document
still works but they are not very useful. Common man-page headings like
DESCRIPTION and OPTIONS appear in the Info node list and they point to
the man page where they appear first (that is git-add currently).
Also, this patch adds directory-entry information for Info document to
make the document appear in the top-level Info directory.
Signed-off-by: Teemu Likonen <tlikonen@iki.fi>
Signed-off-by: Junio C Hamano <gitster@pobox.com>
Diffstat (limited to 'grep.h')
0 files changed, 0 insertions, 0 deletions