Merge branch 'bash_array' into 'master'

Adds to BOB_DOCUMENTATION_SERVER if already set (new bob.extension support)

See merge request !37

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"