@echo "Nothing to do per default, interesting targets:"
@echo
@echo " manual # import the (xhtml version of the) user manual"
@echo "Nothing to do per default, interesting targets:"
@echo
@echo " manual # import the (xhtml version of the) user manual"
@echo " images # build images for the splash screen"
@echo " papers # build the papers page from xml/papers.xml"
@echo
@echo " images # build images for the splash screen"
@echo " papers # build the papers page from xml/papers.xml"
@echo
$(MAKE) -C $(DOCS_SRC_DIR)/ html
rm -rf $(DOCS_DEST_DIR)/*
test -d $(DOCS_DEST_DIR)/ || mkdir -p $(DOCS_DEST_DIR)/
$(MAKE) -C $(DOCS_SRC_DIR) install DESTDIR=$(DOCS_DEST_DIR)/
touch $@
$(MAKE) -C $(DOCS_SRC_DIR)/ html
rm -rf $(DOCS_DEST_DIR)/*
test -d $(DOCS_DEST_DIR)/ || mkdir -p $(DOCS_DEST_DIR)/
$(MAKE) -C $(DOCS_SRC_DIR) install DESTDIR=$(DOCS_DEST_DIR)/
touch $@