commit e0fc56a22bc1b8f1fb0f84fccdad0333da105e02
parent c6dd1d4681637f9126ffd37c71619dab0392cfd1
Author: Jacob R. Edwards <jacob@jacobedwards.org>
Date: Sun, 18 Aug 2024 12:23:18 -0700
Update getlib to not require a git reference
Diffstat:
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/getlib b/getlib
@@ -2,8 +2,11 @@
set -e
-base="${1:%@*}"
-tag="${1#*@}"
+base="${1%%@*}"
+tag="${1##*@}"
+test "$tag" = "$1" &&
+ tag=''
+
url=https://"$base"
dir=lib/"$base"/src
@@ -17,7 +20,8 @@ cd "$dir"
${fetch:-true} &&
git fetch -q
-git checkout -q "$tag"
+test "$tag" &&
+ git checkout -q "$tag"
# Reset would work, but this seems safer
# (In case the git directory is somehow deleted, etc.)