# If dev lab, credentials may not be the default ones, just provide a path to put them into docker
# replace the default one by the customized one provided by jenkins config
if [ -n "${LAB_CONFIG}" ]; then
# If dev lab, credentials may not be the default ones, just provide a path to put them into docker
# replace the default one by the customized one provided by jenkins config
if [ -n "${LAB_CONFIG}" ]; then