#!/bin/bash set -e # Taken from https://git.io/JJOXZ function fetch() { path="examples/$1" url=$2 sha=$3 if [ ! -d "$path" ]; then git clone --depth 1 --branch "$sha" "https://github.com/$url" "$path" fi pushd "$path" >/dev/null git fetch --depth 1 origin "$sha" && git reset --hard "$sha" popd >/dev/null } mkdir -p examples fetch "hack-sql-fake" "slackhq/hack-sql-fake" "v4.0.5" fetch "hack-json-schema" "slackhq/hack-json-schema" "v4.27.1" fetch "hhvm" "facebook/hhvm" "HHVM-4.67.0"