diff --git a/contrib/jenkins.sh b/contrib/jenkins.sh index a3a3d4a2..9ee073d3 100755 --- a/contrib/jenkins.sh +++ b/contrib/jenkins.sh @@ -62,9 +62,5 @@ $MAKE check \ $MAKE $PARALLEL_MAKE distcheck \ || cat-testlogs.sh -if [ "$WITH_MANUALS" = "1" ] && [ "$PUBLISH" = "1" ]; then - make -C "$base/doc/manuals" publish -fi - $MAKE $PARALLEL_MAKE maintainer-clean osmo-clean-workspace.sh