diff options
| -rw-r--r-- | doc/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/Makefile b/doc/Makefile index 878874b..8d2806c 100644 --- a/doc/Makefile +++ b/doc/Makefile | |||
| @@ -151,7 +151,8 @@ dist: doc | |||
| 151 | $(VERB)if [ "$(BOOK_DIST_DIR)" = "" ]; then echo "ERROR: Missing BOOK_DIST_DIR parameter, typically shall be xxx/doc"; exit 10; fi | 151 | $(VERB)if [ "$(BOOK_DIST_DIR)" = "" ]; then echo "ERROR: Missing BOOK_DIST_DIR parameter, typically shall be xxx/doc"; exit 10; fi |
| 152 | $(VERB)if [ ! -d "`dirname $(BOOK_DIST_DIR)`" ]; then echo "ERROR: Missing parent for BOOK_DIST_DIR"; exit 10; fi | 152 | $(VERB)if [ ! -d "`dirname $(BOOK_DIST_DIR)`" ]; then echo "ERROR: Missing parent for BOOK_DIST_DIR"; exit 10; fi |
| 153 | $(VERB)if [ -f "$(BOOK_DIST_DIR)/Makefile" ]; then echo "ERROR: Wrong BOOK_DIST_DIR, contains a Makefile?"; exit 10; fi | 153 | $(VERB)if [ -f "$(BOOK_DIST_DIR)/Makefile" ]; then echo "ERROR: Wrong BOOK_DIST_DIR, contains a Makefile?"; exit 10; fi |
| 154 | $(VERB)if [ ! -d "$(BOOK_DIST_DIR)" ]; then mkdir -p "$(BOOK_DIST_DIR)/pdf" ; fi | 154 | $(VERB)if [ ! -d "$(BOOK_DIST_DIR)" ]; then mkdir -p "$(BOOK_DIST_DIR)" ; fi |
| 155 | $(VERB)if [ ! -d "$(BOOK_DIST_DIR)/pdf" ]; then mkdir -p "$(BOOK_DIST_DIR)/pdf" ; fi | ||
| 155 | $(VERB)for book in $(COMPONENTS); do \ | 156 | $(VERB)for book in $(COMPONENTS); do \ |
| 156 | if ls -d $$book/book*.pdf >/dev/null 2>&1; then cp --preserve=timestamps $$book/book*.pdf "$(BOOK_DIST_DIR)/pdf" ; fi ; \ | 157 | if ls -d $$book/book*.pdf >/dev/null 2>&1; then cp --preserve=timestamps $$book/book*.pdf "$(BOOK_DIST_DIR)/pdf" ; fi ; \ |
| 157 | if ls -d $$book/html >/dev/null 2>&1; then cp -r --preserve=timestamps $$book/html "$(BOOK_DIST_DIR)" ; fi ; \ | 158 | if ls -d $$book/html >/dev/null 2>&1; then cp -r --preserve=timestamps $$book/html "$(BOOK_DIST_DIR)" ; fi ; \ |