Skip to content

Commit

Permalink
[ci] diversified external CI selects a valid branch
Browse files Browse the repository at this point in the history
we need to check existence of a remote branch with refs/heads
(otherwise, we would accept partial matches), but checkout without.
  • Loading branch information
fdupress committed Sep 6, 2024
1 parent e553ce9 commit a2c11f1
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -124,12 +124,12 @@ jobs:
with:
path: easycrypt
- name: Extract target branch name
run: echo "branch=refs/heads/merge-${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}}" >> $GITHUB_OUTPUT
run: echo "branch=merge-${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}}" >> $GITHUB_OUTPUT
id: extract_branch
- name: Find remote branch
id: branch_name
run: |
git ls-remote --exit-code --heads ${{ matrix.target.repository }} ${{ steps.extract_branch.outputs.branch }} || exists=$?
git ls-remote --exit-code --heads ${{ matrix.target.repository }} refs/heads/${{ steps.extract_branch.outputs.branch }} || exists=$?
if [ "$exists" = "2" ];
then echo "REPO_BRANCH=${{ matrix.target.branch }}" >> $GITHUB_OUTPUT;
else echo "REPO_BRANCH=${{ steps.extract_branch.outputs.branch }}" >> $GITHUB_OUTPUT;
Expand Down

0 comments on commit a2c11f1

Please sign in to comment.