diff options
| -rw-r--r-- | Makefile.doc | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile.doc b/Makefile.doc index 5388c6769..d8613471b 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -266,6 +266,8 @@ ide/index_urls.txt: doc/refman/html/index.html # Install all documentation files ###################################################################### +.PHONY: install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-url + install-doc: install-doc-meta install-doc-html install-doc-printable install-doc-index-url install-doc-meta: |