From 8ebead6026605084899efebebecf47f4b64d7ad2 Mon Sep 17 00:00:00 2001
From: Andre Anjos <andre.dos.anjos@gmail.com>
Date: Thu, 12 Jan 2017 16:11:30 +0100
Subject: [PATCH] Adds to BOB_DOCUMENTATION_SERVER if already set (new
bob.extension support)
---
gitlab/functions.sh | 8 +++++++-
1 file changed, 7 insertions(+), 1 deletion(-)
diff --git a/gitlab/functions.sh b/gitlab/functions.sh
index 8b24fca..a42b74e 100644
--- a/gitlab/functions.sh
+++ b/gitlab/functions.sh
@@ -256,7 +256,13 @@ export_env LD_LIBRARY_PATH
export_env BOB_PREFIX_PATH
if [ -z "${CI_BUILD_TAG}" ]; then
- BOB_DOCUMENTATION_SERVER="${DOCSERVER}/software/bob/docs/latest/bob/%s/master/"
+ DEFSRV="${DOCSERVER}/software/bob/docs/latest/bob/%s/master/"
+ if [ -z "${BOB_DOCUMENTATION_SERVER}" ]; then
+ BOB_DOCUMENTATION_SERVER="${DEFSRV}"
+ else
+ BOB_DOCUMENTATION_SERVER="${BOB_DOCUMENTATION_SERVER}|${DEFSRV}"
+ fi
+ unset DEFSRV
export_env BOB_DOCUMENTATION_SERVER
else
log_info "Building tag, not setting BOB_DOCUMENTATION_SERVER"
--
GitLab