jenkins.sh: disable 'publish' of manuals; we don't have any yet

Change-Id: Ib5fb783e4e7e5e327e474344220206f33c64a8bd
This commit is contained in:
Harald Welte 2019-12-04 13:57:24 +01:00
parent b36921fffc
commit 54fc223ab9
1 changed files with 3 additions and 3 deletions

View File

@ -59,9 +59,9 @@ LD_LIBRARY_PATH="$inst/lib" \
$MAKE distcheck \
|| cat-testlogs.sh
if [ "$WITH_MANUALS" = "1" ] && [ "$PUBLISH" = "1" ]; then
make -C "$base/doc/manuals" publish
fi
#if [ "$WITH_MANUALS" = "1" ] && [ "$PUBLISH" = "1" ]; then
# make -C "$base/doc/manuals" publish
#fi
$MAKE maintainer-clean
osmo-clean-workspace.sh