+ @echo
+ @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
+
+clean:
+
+manual: manual-stamp
+manual-stamp: $(DOCS_SRC_DIR)/*.xml
+ $(MAKE) -C $(DOCS_SRC_DIR)/ html
+ test -d $(DOCS_DEST_DIR)/ || mkdir -p $(DOCS_SRC_DIR)/
+ cp $(DOCS_SRC_DIR)/*.html $(DOCS_DEST_DIR)/
+ touch $@