diff options
author | Eric Sunshine <sunshine@sunshineco.com> | 2018-08-31 09:33:18 +0300 |
---|---|---|
committer | Junio C Hamano <gitster@pobox.com> | 2018-08-31 21:49:52 +0300 |
commit | 6f924265a0bf6efa677e9a684cebdde958e5ba06 (patch) | |
tree | 9f0a7b7694aef45c78b89afdcb427123237a9597 /Documentation | |
parent | ad51743007d408ba6f1f670126d57722bb397ce6 (diff) |
doc/Makefile: drop doc-diff worktree and temporary files on "make clean"
doc-diff creates a temporary working tree (git-worktree) and generates a
bunch of temporary files which it does not remove since they act as a
cache to speed up subsequent runs. Although doc-diff's working tree and
generated files are not strictly build products of the Makefile (which,
itself, never runs doc-diff), as a convenience, update "make clean" to
clean up doc-diff's working tree and generated files along with other
development detritus normally removed by "make clean".
Signed-off-by: Eric Sunshine <sunshine@sunshineco.com>
Signed-off-by: Junio C Hamano <gitster@pobox.com>
Diffstat (limited to 'Documentation')
-rw-r--r-- | Documentation/Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Documentation/Makefile b/Documentation/Makefile index d079d7c73a..623f1a866d 100644 --- a/Documentation/Makefile +++ b/Documentation/Makefile @@ -331,6 +331,7 @@ clean: $(RM) SubmittingPatches.txt $(RM) $(cmds_txt) $(mergetools_txt) *.made $(RM) manpage-base-url.xsl + '$(SHELL_PATH_SQ)' ./doc-diff --clean $(MAN_HTML): %.html : %.txt asciidoc.conf $(QUIET_ASCIIDOC)$(RM) $@+ $@ && \ |