contrib/jenkins.sh: split docs-publish

Split publishing of docs into an extra case, so jenkins can run it
separately after generating the docs inside docker. The docs-publish
part will be running outside of docker so the ssh agent works.

Related: OS#5767
Change-Id: I9d3a7089c627f34b63d9f980b8cb6ec7d8158f47
osmith/wip
Oliver Smith 2 months ago
parent 5d26311efc
commit b10f551ac3
  1. 11
      contrib/jenkins.sh

@ -2,9 +2,7 @@
# jenkins build helper script for pysim. This is how we build on jenkins.osmocom.org
#
# environment variables:
# * WITH_MANUALS: build manual PDFs if set to "1"
# * PUBLISH: upload manuals after building if set to "1" (ignored without WITH_MANUALS = "1")
# * JOB_TYPE: one of 'test', 'pylint', 'docs'
# * JOB_TYPE: one of 'test', 'pylint', 'docs', 'docs-publish'
#
export PYTHONUNBUFFERED=1
@ -46,10 +44,9 @@ case "$JOB_TYPE" in
"docs")
rm -rf docs/_build
make -C "docs" html latexpdf
if [ "$WITH_MANUALS" = "1" ] && [ "$PUBLISH" = "1" ]; then
make -C "docs" publish publish-html
fi
;;
"docs-publish")
make -C "docs" publish publish-html
;;
*)
set +x

Loading…
Cancel
Save