From 9efdde23e0858f0925f0d3b4a6df842670b626c9 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 22 Nov 2023 21:56:39 +1100 Subject: [PATCH] fix: most-recently-nightly-tag does not assume a 'nightly' remote (#2947) `script/most-recent-nightly-tag.sh` determines the most recent nightly release in your current git history. Previously it was assuming that you had a `nightly` remote, to pull tags from. Now it just pulls directly from the repository by URL. --- script/most-recent-nightly-tag.sh | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/script/most-recent-nightly-tag.sh b/script/most-recent-nightly-tag.sh index 704c6a2653..c96018955d 100755 --- a/script/most-recent-nightly-tag.sh +++ b/script/most-recent-nightly-tag.sh @@ -1,13 +1,10 @@ #!/bin/bash -# Name of the remote repository -remote_name="nightly" - # Prefix for tags to search for tag_prefix="nightly-" # Fetch all tags from the remote repository -git fetch $remote_name --tags > /dev/null +git fetch git@github.com:leanprover/lean4-nightly.git --tags > /dev/null # Get the most recent commit that has a matching tag tag_name=$(git tag --merged HEAD --list "${tag_prefix}*" | sort -rV | head -n 1 | sed "s/^$tag_prefix//")