diff options
Diffstat (limited to 'Documentation')
| -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 |