diff --git a/Documentation/Makefile b/Documentation/Makefile
index 62269e39c4edf95b2cf2e6a60bff2a33b239b07e..ded0e40b978e6f4b85530541c45782f2b383ea44 100644 (file)
--- a/Documentation/Makefile
+++ b/Documentation/Makefile
INSTALL?=install
RM ?= rm -f
DOC_REF = origin/man
+HTML_REF = origin/html
infodir?=$(prefix)/share/info
MAKEINFO=makeinfo
quick-install:
sh ./install-doc-quick.sh $(DOC_REF) $(DESTDIR)$(mandir)
+quick-install-html:
+ sh ./install-doc-quick.sh $(HTML_REF) $(DESTDIR)$(htmldir)
+
.PHONY: .FORCE-GIT-VERSION-FILE