File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -124,12 +124,12 @@ jobs:
124124 with :
125125 path : easycrypt
126126 - name : Extract target branch name
127- run : echo "branch=refs/heads/ merge-${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}}" >> $GITHUB_OUTPUT
127+ run : echo "branch=merge-${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}}" >> $GITHUB_OUTPUT
128128 id : extract_branch
129129 - name : Find remote branch
130130 id : branch_name
131131 run : |
132- git ls-remote --exit-code --heads ${{ matrix.target.repository }} ${{ steps.extract_branch.outputs.branch }} || exists=$?
132+ git ls-remote --exit-code --heads ${{ matrix.target.repository }} refs/heads/ ${{ steps.extract_branch.outputs.branch }} || exists=$?
133133 if [ "$exists" = "2" ];
134134 then echo "REPO_BRANCH=${{ matrix.target.branch }}" >> $GITHUB_OUTPUT;
135135 else echo "REPO_BRANCH=${{ steps.extract_branch.outputs.branch }}" >> $GITHUB_OUTPUT;
You can’t perform that action at this time.
0 commit comments