diff options
author | Johannes Schindelin <johannes.schindelin@gmx.de> | 2019-03-25 22:41:38 +0100 |
---|---|---|
committer | Junio C Hamano <gitster@pobox.com> | 2019-04-01 07:01:09 +0200 |
commit | 8e6d69591a46b3cb37641f5e99c7fa8b7e896f00 (patch) | |
tree | 5812ae7f8b82bf53ff8fa1fd81e837e423933e31 /Makefile | |
parent | check-docs: really look at the documented commands again (diff) | |
download | git-8e6d69591a46b3cb37641f5e99c7fa8b7e896f00.tar.xz git-8e6d69591a46b3cb37641f5e99c7fa8b7e896f00.zip |
check-docs: do not expect guide pages to correspond to commands
When we want to see what commands are listed in `command-list.txt` but
not installed, we currently include lines that refer to guides, e.g.
`gitattributes` or `gitcli`.
Let's not include those lines, as they are not referring to commands.
Signed-off-by: Johannes Schindelin <johannes.schindelin@gmx.de>
Signed-off-by: Junio C Hamano <gitster@pobox.com>
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -3078,6 +3078,7 @@ check-docs:: ( \ sed -e '1,/^### command list/d' \ -e '/^#/d' \ + -e '/guide$$/d' \ -e 's/[ ].*//' \ -e 's/^/listed /' command-list.txt; \ $(MAKE) -C Documentation print-man1 | \ |