diff --git a/Documentation/Makefile b/Documentation/Makefile
index 4797b2dc3522ccd2050ddefe990268fddb6b8a47..8a8a3954dc45723f7380b59dadbb7e412198d672 100644 (file)
--- a/Documentation/Makefile
+++ b/Documentation/Makefile
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
quick-install-html:
'$(SHELL_PATH_SQ)' ./install-doc-quick.sh $(HTML_REF) $(DESTDIR)$(htmldir)
-.PHONY: .FORCE-GIT-VERSION-FILE
+.PHONY: FORCE