chore: script/most-recent-nightly-tag uses https rather than ssh repo URL (#2951)
The https URL suffices, and does not require that the caller has an appropriate ssh key.
This commit is contained in:
parent
260eaebf4e
commit
a422f3f2c9
1 changed files with 1 additions and 1 deletions
|
|
@ -4,7 +4,7 @@
|
|||
tag_prefix="nightly-"
|
||||
|
||||
# Fetch all tags from the remote repository
|
||||
git fetch git@github.com:leanprover/lean4-nightly.git --tags > /dev/null
|
||||
git fetch https://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