Spaces:
Runtime error
Runtime error
set -e | |
function checkout() { | |
repo=$1; url=$2; sha=$3 | |
if [ ! -d "$repo" ]; then | |
git clone "https://github.com/$url" "$repo" | |
fi | |
pushd "$repo" | |
git fetch && git reset --hard "$sha" | |
popd | |
} | |
checkout examples/codeql github/codeql 86404af50100b409b18e62651295e79393a6016a | |