From 5ad661ef7bdbba5edb312ad82d809dfacd3dc42c Mon Sep 17 00:00:00 2001 From: Hans-Christoph Steiner Date: Thu, 11 Jan 2018 16:47:49 +0100 Subject: [PATCH] jenkins-build-all: use local mediawiki if available --- jenkins-build-all | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/jenkins-build-all b/jenkins-build-all index 3308f61e..66ee3610 100755 --- a/jenkins-build-all +++ b/jenkins-build-all @@ -76,7 +76,19 @@ else fi echo "build_server_always = True" > config.py -$WORKSPACE/fdroid build --verbose --latest --no-tarball --all +# if the local mediawiki is available, then use it +if nc -z -w1 localhost 32445; then + wikiflag="--wiki" + echo "wiki_protocol = 'http'" >> config.py + echo "wiki_server = 'localhost:32445'" >> config.py + echo "wiki_path = '/mediawiki/'" >> config.py + echo "wiki_user = 'fdroid'" >> config.py + echo "wiki_password = 'update.TestCase'" >> config.py +else + sed -i '/^wiki_/d' config.py +fi + +$WORKSPACE/fdroid build --verbose --latest --no-tarball --all $wikiflag vagrant global-status cd builder -- 2.30.2