ci: Use remote pull/merge ref instead of local git merge
The merge strategy on the remote may be different than the local one. This may cause local merges to be different or fail completely. Fix this by using the result of the remote merge. (copied from bitcoin/bitcoin@fad7281d78)
This commit is contained in:
parent
b1579cf5fb
commit
0ecf318851
|
@ -53,11 +53,11 @@ cat_logs_snippet: &CAT_LOGS
|
|||
|
||||
merge_base_script_snippet: &MERGE_BASE
|
||||
merge_base_script:
|
||||
- if [ "$CIRRUS_PR" = "" ]; then exit 0; fi
|
||||
- git fetch $CIRRUS_REPO_CLONE_URL $CIRRUS_BASE_BRANCH
|
||||
- git config --global user.email "ci@ci.ci"
|
||||
- git config --global user.name "ci"
|
||||
- git merge FETCH_HEAD # Merge base to detect silent merge conflicts
|
||||
- if [ "$CIRRUS_PR" = "" ]; then exit 0; fi
|
||||
- git fetch $CIRRUS_REPO_CLONE_URL "pull/${CIRRUS_PR}/merge"
|
||||
- git checkout FETCH_HEAD # Use merged changes to detect silent merge conflicts
|
||||
|
||||
linux_container_snippet: &LINUX_CONTAINER
|
||||
container:
|
||||
|
|
Loading…
Reference in New Issue