File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -123,10 +123,21 @@ jobs:
123123 - uses : actions/checkout@v4
124124 with :
125125 path : easycrypt
126+ - name : Extract target branch name
127+ run : echo "branch=refs/heads/merge-${GITHUB_HEAD_REF:-${GITHUB_REF#refs/heads/}}" >> $GITHUB_OUTPUT
128+ id : extract_branch
129+ - name : Find remote branch
130+ id : branch_name
131+ run : |
132+ git ls-remote --exit-code --heads ${{ matrix.target.repository }} ${{ steps.extract_branch.outputs.branch }} || exists=$?
133+ if [ "$exists" = "2" ];
134+ then echo "REPO_BRANCH=${{ matrix.target.branch }}" >> $GITHUB_OUTPUT;
135+ else echo "REPO_BRANCH=${{ steps.extract_branch.outputs.branch }}" >> $GITHUB_OUTPUT;
136+ fi
126137 - name : Checkout External Project
127138 run : |
128139 git clone --recurse-submodules \
129- -b ${{ matrix.target.branch }} \
140+ -b ${{ steps.branch_name.outputs.REPO_BRANCH }} \
130141 ${{ matrix.target.repository }} \
131142 project/${{ matrix.target.name }}
132143 - name : Install EasyCrypt dependencies
You can’t perform that action at this time.
0 commit comments