Merge branch 'jc/color-attrs'

diff --git a/Documentation/Makefile b/Documentation/Makefile
index 4797b2dc3522ccd2050ddefe990268fddb6b8a47..8a8a3954dc45723f7380b59dadbb7e412198d672 100644 (file)
--- a/Documentation/Makefile
+++ b/Documentation/Makefile
@@ -204,7 +204,7 @@ install-pdf: pdf
 install-html: html
        '$(SHELL_PATH_SQ)' ./install-webdoc.sh $(DESTDIR)$(htmldir)
 
-../GIT-VERSION-FILE: .FORCE-GIT-VERSION-FILE
+../GIT-VERSION-FILE: FORCE
        $(QUIET_SUBDIR0)../ $(QUIET_SUBDIR1) GIT-VERSION-FILE
 
 -include ../GIT-VERSION-FILE
@@ -337,4 +337,4 @@ quick-install-man:
 quick-install-html:
        '$(SHELL_PATH_SQ)' ./install-doc-quick.sh $(HTML_REF) $(DESTDIR)$(htmldir)
 
-.PHONY: .FORCE-GIT-VERSION-FILE
+.PHONY: FORCE