diff options
| author |  Ævar Arnfjörð Bjarmason <avarab@gmail.com> | 2021-10-15 14:39:13 +0200 |
|---|---|---|
| committer |  Junio C Hamano <gitster@pobox.com> | 2021-10-15 10:20:21 -0700 |
| commit | 8cc804d0abf78e5ff22f1561e9301e7264c58aa0 (patch) | |
| tree | d4c283bace8e93387ad60e6bd8c3307d40197a93 | |
| parent | doc lint: emit errors on STDERR (diff) | |
| download | tgif-8cc804d0abf78e5ff22f1561e9301e7264c58aa0.tar.xz | |
doc build: speed up "make lint-docs"
Extend the trick we use to speed up the "clean" target to also extend
to the "lint-docs" target. See 54df87555b1 (Documentation/Makefile:
conditionally include doc.dep, 2020-12-08) for the "clean"
implementation.
The "doc-lint" target only depends on *.txt files, so we don't need to
generate GIT-VERSION-FILE etc. if that's all we're doing. This makes
the "make lint-docs" target more than 2x as fast:
$ git show HEAD~:Documentation/Makefile >Makefile.old
$ hyperfine -L f ",.old" 'make -f Makefile{f} lint-docs'
Benchmark #1: make -f Makefile lint-docs
Time (mean ± σ): 100.2 ms ± 1.3 ms [User: 93.7 ms, System: 6.7 ms]
Range (min … max): 98.4 ms … 103.1 ms 29 runs
Benchmark #2: make -f Makefile.old lint-docs
Time (mean ± σ): 220.0 ms ± 20.0 ms [User: 206.0 ms, System: 18.0 ms]
Range (min … max): 206.6 ms … 267.5 ms 11 runs
Summary
'make -f Makefile lint-docs' ran
2.19 ± 0.20 times faster than 'make -f Makefile.old lint-docs'
Signed-off-by: Ævar Arnfjörð Bjarmason <avarab@gmail.com>
Signed-off-by: Junio C Hamano <gitster@pobox.com>
| -rw-r--r-- | Documentation/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Documentation/Makefile b/Documentation/Makefile index a63627516c..decb77d360 100644 --- a/Documentation/Makefile +++ b/Documentation/Makefile @@ -282,7 +282,7 @@ install-html: html ../GIT-VERSION-FILE: FORCE $(QUIET_SUBDIR0)../ $(QUIET_SUBDIR1) GIT-VERSION-FILE -ifneq ($(MAKECMDGOALS),clean) +ifneq ($(filter-out lint-docs clean,$(MAKECMDGOALS)),) -include ../GIT-VERSION-FILE endif |