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