jenkins.sh: Support for building + publishing the manual

Change-Id: Ic399662e6ac5e5e7f999e6e7127df9a9580a0627
---
M contrib/jenkins.sh
1 file changed, 8 insertions(+), 1 deletion(-)


git pull ssh://gerrit.osmocom.org:29418/osmo-e1d refs/changes/24/30024/1

diff --git a/contrib/jenkins.sh b/contrib/jenkins.sh
index a6ca30e..423e26e 100755
--- a/contrib/jenkins.sh
+++ b/contrib/jenkins.sh
@@ -29,6 +29,9 @@
 
 # Additional configure options and depends
 CONFIG=""
+if [ "$WITH_MANUALS" = "1" ]; then
+	 CONFIG="--enable-manuals"
+fi
 
 set +x
 echo
@@ -44,6 +47,10 @@
 $MAKE $PARALLEL_MAKE
 $MAKE check || cat-testlogs.sh
 DISTCHECK_CONFIGURE_FLAGS="$CONFIG" $MAKE distcheck || cat-testlogs.sh
-$MAKE maintainer-clean
 
+if [ "$WITH_MANUALS" = "1" ] && [ "$PUBLISH" = "1" ]; then
+	make -C "$base/doc/manuals" publish
+fi
+
+$MAKE maintainer-clean
 osmo-clean-workspace.sh

