diff options
author | Junio C Hamano <gitster@pobox.com> | 2021-10-18 15:25:31 -0700 |
---|---|---|
committer | Junio C Hamano <gitster@pobox.com> | 2021-10-18 15:25:31 -0700 |
commit | 5ec7e19bc3e120d0dcf8caaf724cf5274001384a (patch) | |
tree | b6c10c732cd31361d475271491d3ec30d25b5c87 | |
parent | 2d679f40c21efe91581ef430fe197c0e43a20e34 (diff) |
Meta/Dothem: enable check-docs
-rwxr-xr-x | Dothem | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -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 |