diff options
| -rw-r--r-- | libraries/Makefile | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/libraries/Makefile b/libraries/Makefile index 778ffce6d8..1b6546b758 100644 --- a/libraries/Makefile +++ b/libraries/Makefile @@ -335,9 +335,11 @@ binary-dist: $(foreach SUBDIR,$(SUBDIRS),binary-dist.library.$(SUBDIR)) mkdir $(BIN_DIST_LIBDIR)/ifBuildable cp ifBuildable/ifBuildable $(BIN_DIST_LIBDIR)/ifBuildable cp Makefile $(BIN_DIST_LIBDIR) +ifeq "$(HADDOCK_DOCS)" "YES" cp gen_contents_index $(BIN_DIST_LIBDIR) cp index.html $(BIN_DIST_LIBDIR) cp doc-index.html $(BIN_DIST_LIBDIR) +endif cp -pR stamp $(BIN_DIST_LIBDIR) $(foreach SUBDIR,$(SUBDIRS),binary-dist.library.$(SUBDIR)): \ |