chore: pr-release.yaml: create testing branch from tag or branch

.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