File size: 297 Bytes
0c77d6e
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
#!/bin/bash

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