diff options
| -rwxr-xr-x | doc/build.sh | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/doc/build.sh b/doc/build.sh new file mode 100755 index 0000000..699e31d --- /dev/null +++ b/doc/build.sh | |||
| @@ -0,0 +1,19 @@ | |||
| 1 | #!/bin/bash | ||
| 2 | set -e | ||
| 3 | |||
| 4 | # Change PATH environment variable | ||
| 5 | export PATH=/rdtools/docbook/jdk1.6.0_45/bin:/rdtools/docbook/fop-2.1:$PATH | ||
| 6 | |||
| 7 | # Get script arguments | ||
| 8 | docs_path=$1 | ||
| 9 | if [ "$docs_path" = "" ] | ||
| 10 | then | ||
| 11 | echo " usage: build.sh <build_doc_path>" | ||
| 12 | exit | ||
| 13 | fi | ||
| 14 | |||
| 15 | # Build documentation | ||
| 16 | echo make dist BOOK_DIST_DIR=${docs_path} BOOK_DIST_ECLIPSE=yes | ||
| 17 | make dist BOOK_DIST_DIR=${docs_path} BOOK_DIST_ECLIPSE=yes | ||
| 18 | |||
| 19 | echo "Build documentation was successful. Documentation can be found here ${docs_path}" | ||
