summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorJunio C Hamano <gitster@pobox.com>2021-10-18 15:25:31 -0700
committerJunio C Hamano <gitster@pobox.com>2021-10-18 15:25:31 -0700
commit5ec7e19bc3e120d0dcf8caaf724cf5274001384a (patch)
treeb6c10c732cd31361d475271491d3ec30d25b5c87
parent2d679f40c21efe91581ef430fe197c0e43a20e34 (diff)
Meta/Dothem: enable check-docs
-rwxr-xr-xDothem1
1 files changed, 1 insertions, 0 deletions
diff --git a/Dothem b/Dothem
index 84b620c671..82cca97a96 100755
--- a/Dothem
+++ b/Dothem
@@ -216,6 +216,7 @@ do
test -n "$skip_doc" ||
if test "$save" = "$(git rev-parse HEAD)"
then
+ Meta/Make $M $jobs -- check-docs &&
Meta/Make $M $jobs -- doc &&
Meta/Make $M -- install-man install-html
else