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.
This commit is contained in:
parent
91917516f1
commit
9efdde23e0
1 changed files with 1 additions and 4 deletions
|
|
@ -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//")
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue