#!/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}