From bd7b7b778b6e6abc7df634a43f0c3cb11618989d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jordi=20Guti=C3=A9rrez=20Hermoso?= <jordigh@octave.org>
Date: Wed, 19 Jun 2024 12:18:34 -0400
Subject: [PATCH] checkout-ext-directory: new helper script

This is just a helper script to get the ext directory of other grist
repos, currently intended for grist-ee.
---
 buildtools/checkout-ext-directory.sh | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100755 buildtools/checkout-ext-directory.sh

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