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}" | ||