+ echo "HADDOCK_DOCS = $(HADDOCK_DOCS)" >> $(BIN_DIST_MK)
+ echo "LATEX_DOCS = $(LATEX_DOCS)" >> $(BIN_DIST_MK)
+ echo "BUILD_DOCBOOK_HTML = $(BUILD_DOCBOOK_HTML)" >> $(BIN_DIST_MK)
+ echo "BUILD_DOCBOOK_PS = $(BUILD_DOCBOOK_PS)" >> $(BIN_DIST_MK)
+ echo "BUILD_DOCBOOK_PDF = $(BUILD_DOCBOOK_PDF)" >> $(BIN_DIST_MK)