#!/bin/bash
# Clone repository if necessary
if [ ! -d "${REPO_DEST}" ]; then
git clone "${REPO_URL}" "${REPO_DEST}"
fi
cd "${REPO_DEST}"
# Update local repository
git fetch
# Checkout repository ref
git checkout ${REPO_REF}