# 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
fi
# 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
fi