diff --git a/buildtools/checkout-ext-directory.sh b/buildtools/checkout-ext-directory.sh new file mode 100755 index 00000000..6861b9e2 --- /dev/null +++ b/buildtools/checkout-ext-directory.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash + +# This checks out the ext/ directory from the extra repo (e.g. +# grist-ee or grist-desktop) depending on the supplied repo name. + +set -e + +repo=$1 +dir=$(dirname $0) +ref=$(cat $dir/.$repo-version) + +git clone --branch $ref --depth 1 --filter=tree:0 "https://github.com/gristlabs/$repo" +pushd $repo +git sparse-checkout set ext +git checkout +popd +mv $repo/ext . +rm -rf $repo