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)
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)