diff options
Diffstat (limited to 'libraries/Makefile')
-rw-r--r-- | libraries/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/libraries/Makefile b/libraries/Makefile index 20a7678023..ce28841320 100644 --- a/libraries/Makefile +++ b/libraries/Makefile @@ -366,7 +366,7 @@ endif echo $(WHERE_AM_I)/ifBuildable/ifBuildable >> $(BIN_DIST_LIST) for FILE in dph/dph-prim-interface/interface/*.h dph/dph/LICENSE; do if [ -f $$FILE ]; then echo $(WHERE_AM_I)/$$FILE >> $(BIN_DIST_LIST); fi; done ifeq "$(HADDOCK_DOCS)" "YES" - for FILE in gen_contents_index prologue index.html doc-index*.html; do echo $(WHERE_AM_I)/$$FILE >> $(BIN_DIST_LIST); done + for FILE in gen_contents_index prologue.txt index.html doc-index*.html; do echo $(WHERE_AM_I)/$$FILE >> $(BIN_DIST_LIST); done endif $(foreach SUBDIR,$(SUBDIRS),binary-dist.library.$(SUBDIR)): \ |