jenkins.sh: Support for building + publishing the manual

Change-Id: Ic399662e6ac5e5e7f999e6e7127df9a9580a0627
---
M contrib/jenkins.sh
1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/contrib/jenkins.sh b/contrib/jenkins.sh
index a6ca30e..6cac702 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
@@ -43,7 +46,14 @@
 ./configure --enable-sanitize --enable-werror $CONFIG
 $MAKE $PARALLEL_MAKE
 $MAKE check || cat-testlogs.sh
-DISTCHECK_CONFIGURE_FLAGS="$CONFIG" $MAKE distcheck || cat-testlogs.sh
-$MAKE maintainer-clean
+# Do distcheck with --disable-manuals as workaround, because it doesn't build
+# the usermanual pdf for some reason and then fails at "make install" because
+# it doesn't exist. Spent a lot of time on debugging it, not worth fixing now.
+DISTCHECK_CONFIGURE_FLAGS="$CONFIG --disable-manuals" $MAKE distcheck || cat-testlogs.sh
 
+if [ "$WITH_MANUALS" = "1" ] && [ "$PUBLISH" = "1" ]; then
+	make -C "$base/doc/manuals" publish
+fi
+
+$MAKE maintainer-clean
 osmo-clean-workspace.sh

