diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 5477d34fdf31..6473cfa17aa4 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -255,7 +255,7 @@ jobs: BASE=nightly-testing fi - echo "Using base branch: $BASE" + echo "Using base tag or branch: $BASE" EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)" echo "Branch exists: $EXISTS" @@ -308,7 +308,7 @@ jobs: if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; 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'." + echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Mathlib. Falling back to 'nightly-testing'." BASE=nightly-testing fi @@ -318,7 +318,9 @@ jobs: echo "Branch exists: $EXISTS" if [ "$EXISTS" = "0" ]; then echo "Branch does not exist, creating it." - git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE" + # Different syntax needed for creating off a branch and off a tag, try both. + git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE" || + git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "origin/$BASE" echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain git add lean-toolchain sed -i "s/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \".\+\"/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean