Skip to content

Commit

Permalink
chore: CI looks for nightly-testing-YYYY-MM-DD at Mathlib as either a…
Browse files Browse the repository at this point in the history
… branch or tag
  • Loading branch information
kim-em committed Jan 19, 2024
1 parent ec30da8 commit bdde13e
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions .github/workflows/pr-release.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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."
Expand Down Expand Up @@ -239,7 +239,7 @@ jobs:
git config user.name "leanprover-community-mathlib4-bot"
git config user.email "[email protected]"
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'."
Expand Down

0 comments on commit bdde13e

Please sign in to comment.