This is just a helper script to get the ext directory of other grist repos, currently intended for grist-ee.pull/1066/head
parent
36f897fd35
commit
bd7b7b778b
@ -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
|
Loading…
Reference in new issue