From bdde13e01f509c25eaf5be4a40f1905fd34692ad Mon Sep 17 00:00:00 2001 From: Scott Morrison <scott.morrison@gmail.com> Date: Fri, 19 Jan 2024 12:33:19 +1100 Subject: [PATCH] chore: CI looks for nightly-testing-YYYY-MM-DD at Mathlib as either a branch or tag --- .github/workflows/pr-release.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 09a9341d2ce0..f9e267daac41 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -126,7 +126,7 @@ jobs: if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then echo "The merge base of this PR coincides with the nightly release" - REMOTE_BRANCHES="$(git ls-remote -h https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")" + REMOTE_BRANCHES="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")" if [[ -n "$REMOTE_BRANCHES" ]]; then echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' branch." @@ -239,7 +239,7 @@ jobs: git config user.name "leanprover-community-mathlib4-bot" git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com" - if git branch -r | grep -q "nightly-testing-${MOST_RECENT_NIGHTLY}"; then + if git ls-remote --heads --tags origin | grep -q "refs/\(heads\|tags\)/nightly-testing-${MOST_RECENT_NIGHTLY}"; then BASE="nightly-testing-${MOST_RECENT_NIGHTLY}" else echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."