From c65e72b6a926b72c88482883caf4b5b23a403aed Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 27 Jan 2024 18:03:40 -0800 Subject: [PATCH] Get `git-clone-related` from git-scripts repository, not plume-scripts --- test.sh | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/test.sh b/test.sh index 625c6cfb..8a414d12 100755 --- a/test.sh +++ b/test.sh @@ -36,12 +36,13 @@ export JAVA_HOME export DAIKONDIR="${DAIKONDIR:-$(pwd)/../daikon}" echo "DAIKONDIR=$DAIKONDIR" -if [ -d "/tmp/plume-scripts" ] ; then - (cd /tmp/plume-scripts && git -C pull -q) > /dev/null 2>&1 + +if [ -d "/tmp/git-scripts" ] ; then + (cd /tmp/git-scripts && git -C pull -q) > /dev/null 2>&1 else - (cd /tmp && git clone --depth 1 -q https://github.com/plume-lib/plume-scripts.git) + (cd /tmp && git clone --depth 1 -q https://github.com/plume-lib/git-scripts.git) fi -/tmp/plume-scripts/git-clone-related codespecs daikon +/tmp/git-scripts/git-clone-related codespecs daikon ln -s "$(pwd)" "${DAIKONDIR}/fjalar" || true make build